A taxonomy of fairness and temporal logic problems for Petri nets (Q805257)

A temporal logic for reasoning about Petri nets is defined, extending the ideas from \textit{R. R. Howell} and \textit{L. E. Rosier} [Theor. Comput. Sci. 64, No.3, 305-329 (1989; Zbl 0673.68040)]. The paper is also strongly related to the ideas from \textit{R. R. Howell}, \textit{L. E. Rosier} and \textit{Hsu-Chun Yen} [Theor. Comput. Sci. 80, No.1, 77-104 (1991; to appear)]. It is shown that the model checking problem for the temporal logic for reasoning about Petri nets is PTIME-equivalent to the Petri net reachability problem.