Petri Nets, Traces, and Local Model Checking

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