zbMATH — the first resource for mathematics

An algorithm for the general Petri net reachability problem. (English) Zbl 0563.68057
An algorithm is presented for the reachability problem in general vector addition systems or Petri nets, two basically equivalent concepts. A vector addition system is characterized by a finite set V of integer vectors \(v^ i\in {\mathbb{Z}}^ m\), and some initial vector w. The reachability set R(V,w) is the minimal set which contains w and, whenever w’ is in the set and \(w'+v^ i\geq 0\), also contains \(w'+v^ i\). The general reachability problem is to decide, given V, w and v, whether \(v\in R(V,w)\). The difficulty of the problem stems from the fact that all intermediate vectors on a ”path” from w to v have to be nonnegative. Finite automata are used in the algorithm to approximate such paths, with the approximation error assessed by Presburger expressions. The approximation algorithm is iterated until a criterion sufficient for reachability becomes satisfied. The proof of termination relies on the well-foundedness of \(N^ m\) under the lexicographic ordering. The exact computational complexity of the algorithm remains an open problem. Only an exponential space lower bound is known. The paper also provides a list of other problems in various areas of mathematics and computer science equivalent with or reducible to the reachability problem.

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03B25 Decidability of theories and sets of sentences
68Q25 Analysis of algorithms and problem complexity
03D15 Complexity of computation (including implicit computational complexity)
03D40 Word problems, etc. in computability and recursion theory
03D05 Automata and formal grammars in connection with logical questions
Full Text: DOI