zbMATH — the first resource for mathematics

Interleaving based model checking of concurrency and causality. (English) Zbl 1397.68123
Summary: We consider a spectrum of properties proposed in [A. Polyvyanyy et al., Lect. Notes Comput. Sci. 8489, 210–232 (2014; Zbl 1393.68123)]. It is related to causality and concurrency between a pair of given transitions in a place/transition net. For each of these properties, we ask whether it can be verified using an ordinary, interleaving based, model checker. With a systematic approach based on two constructions, we reduce most properties in the spectrum to a reachability problem. Only one problem needs to be left open completely. Some problems can be solved only under the assumption of absent auto-concurrency.
68Q60 Specification and verification (program logics, model checking, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: DOI