An Algorithm for the General Petri Net Reachability Problem

An algorithm is presented for the general Petri net reachability problem. It is based on a generalization of the basic reachability tree construction which is made symmetric with respect to the initial and final marking. Sets of transition sequences described by finite automata are used for approximations to firing sequences, and the approximation error is assessed by Presburger expressions. The approximation algorithm is iterated until a sufficient criterion for reachability is satisfied. The exact computational complexity of our algorithm is an open problem.