Technical Report 88--4. Ames, Iowa: State University, Department of Computer Science,, January 1988.
Abstract: The authors define a temporal logic for reasoning about Petri nets. They show the model checking problem for this logic to be PTIME equivalent to the Petri net reachability problem. Using this logic, they show the fair nontermination problem to be PTIME equivalent to the 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, 42 versions of fairness are examined.