Coverability and Termination in Recursive Petri Nets

Alain Finkel 1, 2 Serge Haddad 1, 2, 3 Igor Khmelnitsky 1, 2, 3
3 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
Abstract : In the early two-thousands, Recursive Petri nets have been introduced in order to model distributed planning of multi-agent systems for which counters and recursivity were necessary. Although Recursive Petri nets strictly extend Petri nets and stack automata, most of the usual property problems are solvable but using non primitive recursive algorithms, even for coverability and termination. For almost all other extended Petri nets models containing a stack the complexity of coverability and termination are unknown or strictly larger than EXPSPACE. In contrast, we establish here that for Recursive Petri nets, the coverability and termination problems are EXPSPACE-complete as for Petri nets. From an expressiveness point of view, we show that coverability languages of Recursive Petri nets strictly include the union of coverability languages of Petri nets and context-free languages. Thus we get for free a more powerful model than Petri net.
Document type :
Conference papers
Complete list of metadatas
Contributor : Igor Khmelnitsky <>
Submitted on : Tuesday, April 16, 2019 - 1:56:40 PM
Last modification on : Wednesday, April 17, 2019 - 9:55:00 AM


Coverability and Termination i...
Files produced by the author(s)


  • HAL Id : hal-02081019, version 1


Alain Finkel, Serge Haddad, Igor Khmelnitsky. Coverability and Termination in Recursive Petri Nets. Proceedings of the 40th International Conference on Application and Theory of Petri Nets and Concurrency, Jun 2019, Aachen, Germany. ⟨hal-02081019⟩



Record views


Files downloads