Alain Finkel ; Serge Haddad ; Igor Khmelnitsky - Coverability, Termination, and Finiteness in Recursive Petri Nets

fi:8483 - Fundamenta Informaticae, December 23, 2021, Volume 183, Issues 1-2: Petri Nets 2019
Coverability, Termination, and Finiteness in Recursive Petri NetsArticle

Authors: Alain Finkel ; Serge Haddad ; Igor Khmelnitsky

    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 context-free grammars, most of the usual problems (reachability, coverability, finiteness, boundedness and termination) were known to be solvable by using non-primitive recursive algorithms. 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, termination, boundedness and finiteness 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 a more powerful model than Petri net for free.


    Volume: Volume 183, Issues 1-2: Petri Nets 2019
    Published on: December 23, 2021
    Accepted on: September 22, 2021
    Submitted on: September 15, 2021
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Formal Languages and Automata Theory

    Consultation statistics

    This page has been seen 198 times.
    This article's PDF has been downloaded 201 times.