Petri Nets, Traces, and Local Model Checking

Allan Cheng

In 6th NWPT, pages 142-156

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. By 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 labeled 1-safe nets. It turns out that Mazurkiewicz trace theory provides a useful setting in which the progress fairness assumptions can be formalized in a natural way. We provide the first, to our knowledge, set of sound and complete tableau rules for a CTL-like logic interpreted under progress fairness assumptions.

Comments
BRICS, Department of Computer Science, University of Aarhus, Ny Munkegade, DK-8000 Aarhus C, Denmark. Email: acheng@daimi.aau.dk.

Available as PostScript.

BRICS WWW home page