Petri Nets, Traces, and Local Model Checking

  • Allan Cheng

Abstract

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

Published
1995-06-09
How to Cite
Cheng, A. (1995). Petri Nets, Traces, and Local Model Checking. BRICS Report Series, 2(39). https://doi.org/10.7146/brics.v2i39.19941