For the most recent entries see the Petri Nets Newsletter.

Petri nets, traces and local model checking.

Cheng, Allan

In: Theoretical Computer Science, Vol. 183, pages 229-251. 1997.

Abstract: It has been observed that representing concurrent behaviour as sequences of interleaved events is not satisfactory - not all sequences should be considered as likely behaviours. Taking progress fairness assumptions into account one obtains a more realistic behavioural view of concurrent 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 labelled 1-safe nets. It turns out that Mazurkiewicz trace theory provides a natural setting in which 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,Model-checking; Maximal traces; Partial orders; Inevitability.


Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography