Problems concerning fairness and temporal logic for conflict-free Petri nets (Q1121023)

This paper is identical to the author's work [Advances in Petri Nets, Lect. Notes Comput. Sci. 340, 200-226 (1988)] except for the improvement of Section 4 about model checking. The complexity of the fair nontermination problem is studied for conflict-free Petri nets under several definitions of fairness. The question of determining whether a given structure defines a model of a specification expressed in temporal logic is proved to be undecidable for conflict-free Petri nets. Even if the logic is severely restricted, it is still not feasible: although it becomes decidable, it is then NP-complete.