Abstract
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 the algorithm is an open problem.
| Original language | English |
|---|---|
| Pages (from-to) | 441-460 |
| Number of pages | 20 |
| Journal | SIAM Journal on Computing |
| Volume | 13 |
| Issue number | 3 |
| DOIs | |
| State | Published - 1984 |
| Externally published | Yes |