An algorithm for the general Petri net reachability problem.

*(English)*Zbl 0563.68057An 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.

##### MSC:

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 |