We consider a spectrum of properties proposed in [14], that 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 75% of the properties in the spectrum to a reachability problem. We have to leave the remaining 25% as open problems.
CITATION STYLE
Wolf, K. (2017). Model checking concurrency and causality. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10258 LNCS, pp. 159–178). Springer Verlag. https://doi.org/10.1007/978-3-319-57861-3_11
Mendeley helps you to discover research relevant for your work.