Put your Model Checker on Diet: Verification on Local States

Net unfoldings are a well-known partial order semantics for Petri nets, very suited to act as models for branching-time logics interpreted on local states. We demonstrate how these local logics (in particular a distributed $\mu$-calculus) can be used to express properties from the point of view of one component in a distributed system. Thus -- in contrast to interleaving branching time logics -- in general they do not refer to the entire space of global states. We show that verification of local properties can be done by applying standard model checking algorithms known for interleaving branching time logics. The key is to extract a finite (usually small), local transition system bisimilar to the unfolding. The construction is based on the finite prefix of a net unfolding defined by McMillan.     «

Net unfoldings are a well-known partial order semantics for Petri nets, very suited to act as models for branching-time logics interpreted on local states. We demonstrate how these local logics (in particular a distributed $\mu$-calculus) can be used to express properties from the point of view of one component in a distributed system. Thus -- in contrast to interleaving branching time logics -- in general they do not refer to the entire space of global states. We show that verification of local...     »