A unified approach for deciding the existence of certain petri net paths (Q1184737)

An elegant unified approach for deriving complexity results for a number of Petri net problems is developed. First, the author defines a class of Petri net path formulas, each of which consisting of marking variables, variables for transition sequences, terms, transition predicates and marking predicates. It is shown that the satisfiability problem for such formulas is solvable in \({\mathcal O}(2^{d\times n\times\log n})\) space in the size of the Petri net and the formula (i.e., \(n\)), for some constant \(d\). Consequently, the satisfiability problem is EXPSPACE complete. The usefulness of this result is that many Petri net problems, some of which were previously unsolved, can be reduced to the satisfiability problem and hence they can be solvable in EXPSPACE.