Tutorial: The reachability problem for Petri nets

Systems equipped with counters are central when modeling distributed protocols, programs with recursive parallel threads, programs with pointers, broadcast protocols, databases, etc. When it comes to model-checking counter systems and their variants, the main results are that verification is undecidable when zero-tests are allowed, while several problems can be decided when zero-tests are forbidden - one speaks of VASS, for "vector addition systems with states", or equivalently "Petri nets". In the case of Petri nets, reachability was shown decidable in 1982, and the reachability problem for Petri nets and related decidable problems on subclasses of counter systems are pivot problems not only for the verification of infinite-state systems but also for problems appearing in very active research areas related to various logics and automata for data words/trees. Hence, the design of efficient algorithms for the reachability problem for VASS may have a great impact, not only in the realm of formal verification. It is however a very difficult problem. Therefore, improving the computational cost for solving the reachability problem for Petri nets would also improve the complexity of the formal verification of numerous classes of infinite-state systems. Strikingly, the decision algorithm for Petri net reachability has never been implemented. This is because of its high complexity, both conceptual (the algorithm is very hard to understand and to describe) and computational (it is assumed that the complexity of the algorithm is not primitive-recursive). The general problem is known to be decidable by algorithms exclusively based on the classical Kosaraju-Lambert-Mayr-Sacerdote-Tenney decomposition (KLMTS decomposition). Recently, from this decomposition, it was proved that a final configuration is not reachable from an initial one if, and only if, there exists a Presburger inductive invariant that contains the initial configuration but not the final one. Since we can decide if a Presburger formula denotes an inductive invariant, we deduce from this result that there exist checkable certificates of non-reachability in the Presburger arithmetic. In particular, there exists a simple algorithm for deciding the general Petri net reachability problem based on two semi-algorithms. A first one that tries to prove reachability by enumerating finite sequences of actions and a second one that tries to prove non-reachability by enumerating Presburger formulas. In this presentation, we provide a simple proof of the Petri net reachability problem that is not based on the KLMST decomposition. The proof is based on the notion of production relations, inspired from Hauschildt, that directly proves the existence of Presburger inductive invariants. 13: 00 14: 30 Lunch

Authors

• Jérôme Leroux

Keywords

No keywords are indexed for this paper.