In: Theoretical Computer Science, Vol. 82, No. 2, pages 341-372. May 1991.
Abstract: The authors define a temporal logic for reasoning about Petri nets and show the model checking problem for this logic to be PTIME equivalent to the Petri net reachability problem. Using this logic and two refinements, they show the fair nontermination problem to be PTIME equivalent to reachability for several definitions of fairness. For other versions of fairness, this problem is shown to be either PTIME equivalent to the boundedness problem or highly undecidable. In all, 24 versions of fairness are examined.
Keywords: fairness; temporal logic; model checking problem; reachability problem; fairness; boundedness problem;or highly undecidable. In.