Interleaving Based Model Checking of Concurrency and Causality
Karsten Wolf · Fundamenta Informaticae · 2018
We consider a spectrum of properties proposed in [14]. 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 ap proach 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.