Technical Report 89--11, pages 1-18 pp.. Ames, Iowa: State University, Department of Computer Science, August 1989.
Abstract: The author defines a first order logic for reasoning about Petri nets. The author shows that the satisfiability problem for this logic is EXPSPACE complete. Using this logic, a wide range of Petri net problems can be reduced to the satisfiability problem. Thus, this logic offers an umbrella under which many Petri net problems can be shown to be solvable in EXPSPACE.
Keywords: first order logic (for reasoning about nets); satisfiability problem.