zbMATH — the first resource for mathematics

A taxonomy of fairness and temporal logic problems for Petri nets. (English) Zbl 0655.68072
Mathematical foundations of computer science 1988, Proc. 13th Symp., Carlsbad/Czech. 1988, Lect. Notes Comput. Sci. 324, 351-359 (1988).
[For the entire collection see Zbl 0643.00024.]
The complexity of the fair nontermination problem (NTP), which is to determine whether there exists an infinite transition sequence in a given Petri net, is studied with respect to 24 different notions of fairness which all have been proposed in different papers. Temporal logic is used to express fairness constraints and for reducing NTP’s to the reachability problem for Petri nets.
Others have been shown to be equivalent to the boundedness problem. The paper contains, discusses and improves many of the known results spread over the literature.
Reviewer: M.Jantzen

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
68Q25 Analysis of algorithms and problem complexity