Petri Nets, Traces, and Local Model Checking

  • Allan Cheng


It has been observed that the behavioural view of concurrent
systems that all possible sequences of actions are relevant is too generous;
not all sequences should be considered as likely behaviours. Taking
progress fairness assumptions into account one obtains a more realistic
behavioural view of the systems. In this paper we consider the problem
of performing model checking relative to this behavioural view. We
present a CTL-like logic which is interpreted over the model of concurrent
systems labelled 1-safe nets. It turns out that Mazurkiewicz trace
theory provides a natural setting in which the progress fairness assumptions
can be formalized. We provide the first, to our knowledge, set of
sound and complete tableau rules for a CTL-like logic interpreted under
progress fairness assumptions.

keywords: fair progress, labelled 1-safe nets, local model checking, maximal traces, partial orders, inevitability

How to Cite
Cheng, A. (1995). Petri Nets, Traces, and Local Model Checking. BRICS Report Series, 2(39).