Petri Nets, Traces, and Local Model Checking

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