Coverability, Termination, and Finiteness in Recursive Petri Nets

• Autorzy: Finkel Alaina , Haddad Sergeb , Khmelnitsky Igor

Identyfikatory

DOI

10.3233/FI-2021-2081

• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

Recursive Petri nets; expressiveness; complexity; coverability; termination; finiteness

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2021
• Tom: Vol. 183, nr 1-2
• Strony: 33--66
• Opis fizyczny: Bibliogr., 37 poz., rys.

Twórcy

autor

Finkel Alaina

• Université Paris-Saclay, Gif-sur-Yvette, France

autor

Haddad Sergeb

• LSV, ENS Paris-Saclay, CNRS, INRIA, Université Paris-Saclay, Gif-sur-Yvette, France.

autor

Khmelnitsky Igor

• LSV, ENS Paris-Saclay, CNRS, INRIA, Université Paris-Saclay, Gif-sur-Yvette, France

Bibliografia

• [1] Mayr EW. An Algorithm for the General Petri Net Reachability Problem. SIAM J. Comput., 1984. 13(3):441-460.
• [2] Czerwinski W, Lasota S, Lazic R, Leroux J, Mazowiecki F. The reachability problem for Petri nets is not elementary. In: Proceedings of STOC 19. 2019 pp. 24-33. doi:10.1145/3313276.3316369.
• [3] Leroux J, Schmitz S. Reachability in Vector Addition Systems is Primitive-Recursive in Fixed Dimension. In: Proceedings of LICS 19. 2019 pp. 1-13. doi:10.1109/LICS.2019.8785796.
• [4] Rackoff C. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 1978. 6(2):223 - 231.
• [5] Reinhardt K. Reachability in Petri Nets with Inhibitor Arcs. Electr. Notes Theor. Comput. Sci., 2008. 223:239-264. doi:10.1016/j.entcs.2008.12.042.
• [6] Bonnet R, Finkel A, Leroux J, Zeitoun M. Model Checking Vector Addition Systems with one zero-test. LMCS, 2012. 8(2:11). doi:10.2168/LMCS-8 (2:11).
• [7] Bonnet R. The Reachability Problem for Vector Addition System with One Zero-Test. In: MFCS 2011, Warsaw, Poland, volume 6907 of LNCS. 2011 pp. 145-157. doi:10.1007/978-3-642-22993-0 16. [8] Schnoebelen Ph. Revisiting Ackermann-Hardness for Lossy Counter Machines and Reset Petri Nets. In: MFCS 2010, Brno, Czech Republic, volume 6281 of LNCS. 2010 pp. 616-628. doi:10.1007/978-3-642-15155-2 54.
• [9] Dufourd C, Finkel A, Schnoebelen Ph. Reset Nets between Decidability and Undecidability. In: ICALP’98, volume 1443 of LNCS. Springer, Aalborg, Denmark, 1998 pp. 103-115. doi:10.1007/BFb0055044.
• [10] Lazi´c R, Schmitz S. The Complexity of Coverability in ν-Petri Nets. In: LICS 2016. ACM Press, New York, United States, 2016 pp. 467-476. doi:10.1145/2933575.2933593.
• [11] Lazic R. The reachability problem for vector addition systems with a stack is not elementary. CoRR, 2013. abs/1310.1767. 1310.1767.
• [12] Lazic R, Schmitz S. Non-elementary complexities for branching VASS, MELL, and extensions. In: CSL-LICS 2014, Vienna, Austria. ACM, 2014 pp. 61:1-61:10. doi:10.1145/2733375.
• [13] Demri S, Jurdzi´nski M, Lachish O, Lazi´c R. The covering and boundedness problems for branching vector addition systems. Journal of Computer and System Sciences, 2012. 79(1):23-38. doi:10.1016/j.jcss.2012.04.002.
• [14] Atig MF, Ganty P. Approximating Petri Net Reachability Along Context-free Traces. In: FSTTCS 2011, Mumbai, India, volume 13 of LIPIcs. 2011 pp. 152-163. doi:10.4230/LIPIcs.FSTTCS.2011.152.
• [15] Mavlankulov G, Othman M, Turaev S, Selamat MH, Zhumabayeva L, Zhukabayeva T. Concurrently controlled grammars. Kybernetika, 2018. 54(4):748-764. doi:10.14736/kyb-2018-4-0748. [16] Dassow J, Turaev S. Petri Net Controlled Grammars: the Case of Special Petri Nets. J. UCS, 2009.15(14):2808-2835.
• [17] Zetzsche G. The Emptiness Problem for Valence Automata or: Another Decidable Extension of Petri Nets. In: RP 2015, Warsaw, Poland, volume 9328 of LNCS. 2015 pp. 166-178.
• [18] El Fallah Seghrouchni A, Haddad S. A Recursive Model for Distributed Planning. In: ICMAS 1996, Kyoto, Japan. 1996 pp. 307-314. ISBN:978-1-57735-013-2.
• [19] Haddad S, Poitrenaud D. Theoretical Aspects of Recursive Petri Nets. In: ICATPN 1999, Williamsburg, Virginia, USA, volume 1639 of LNCS. 1999 pp. 228-247. doi:10.1007/3-540-48745-X 14.
• [20] Haddad S, Poitrenaud D. Modelling and Analyzing Systems with Recursive Petri Nets. In: WODES 2000, Ghent, Belgium, volume 569 of The Springer International Series in Engineering and Computer Science. 2000 pp. 449-458. doi:10.1007/978-1-4615-4493-7 48.
• [21] Haddad S, Poitrenaud D. Checking Linear Temporal Formulas on Sequential Recursive Petri Nets. In: TIME 2001, Civdale del Friuli, Italy. IEEE Computer Society, 2001 pp. 198-205. doi:10.1109/TIME.2001.930718.
• [22] Haddad S, Poitrenaud D. Recursive Petri nets. Acta Inf., 2007. 44(7-8):463-508. doi:10.1007/s00236-007-0055-y.
• [23] Finkel A, Haddad S, Khmelnitsky I. Coverability and Termination in Recursive Petri Nets. In: PETRI NETS’19, volume 11522 of LNCSs. Springer, Aachen, Germany, 2019 pp. 429-448. HAL Id:hal-02081019, URL https://hal.inria.fr/hal-02081019.
• 24] Stadel M. A remark on the time complexity of the subtree problem. Computing, 1978. 19(4):297-302.
• [25] Finkel A, Schnoebelen P. Well-structured transition systems everywhere! Theor. Comput. Sci., 2001. 256(1-2):63-92. doi:10.1016/S0304-3975(00)00102-X.
• [26] Czerwinski W, Lasota S, Lazic R, Leroux J, Mazowiecki F. The reachability problem for Petri nets is not elementary. In: STOC 2019. ACM, 2019 pp. 24-33. arXiv:1809.07115 [cs.FL].
• [27] Peterson JL. Petri net theory and the modeling of systems / James L. Peterson. Prentice-Hall Englewood Cliffs, N.J, 1981. ISBN:0136619835.
• [28] Geeraerts G, Raskin J, Begin LV. Well-structured languages. Acta Informatica, 2007. 44(3-4):249-288. doi:10.1007/s00236-007-0050-3.
• [29] Bonnet R, Finkel A, Haddad S, Rosa-Velardo F. Ordinal Theory for Expressiveness of Well-Structured Transition Systems. Information and Computation, 2013. 224:1-22. doi:10.1016/j.ic.2012.11.003.
• [30] Delzanno G, Rosa-Velardo F. On the coverability and reachability languages of monotonic extensions of Petri nets. Theor. Comput. Sci., 2013. 467:12-29. doi:10.1016/j.tcs.2012.09.021.
• [31] Valk R, Vidal-Naquet G. Petri Nets and Regular Languages. J. Comput. Syst. Sci., 1981. 23(3):299-325.[32] Figueira D. Co-finiteness of VASS coverability languages, 2019. Working paper or preprint, URL https: //hal.archives-ouvertes.fr/hal-02193089.
• [33] Hofman P, Totzke P. Trace Inclusion for One-Counter Nets Revisited. In: RP 2014, volume 8762 of LNCS.Springer, 2014 pp. 151-162. doi:10.1007/978-3-319-11439-2 12.
• [34] Haddad S, Poitrenaud D. Decidability and undecidability results for recursive Petri nets. Technical Report 019, LIP6, Paris VI University, 1999. Id: hal-02548232, URL https://hal.archives-ouvertes.fr/hal-02548232.
• [35] Ogden W. A helpful result for proving inherent ambiguity. Mathematical systems theory, 1968. 2(3):191-194. doi:10.1007/BF01694004.
• [36] Lambert J. A Structure to Decide Reachability in Petri Nets. Theor. Comput. Sci., 1992. 99(1):79-104. doi:10.1016/0304-3975(92)90173-D.
• [37] Lipton RJ. The Reachability Problem Requires Exponential Space. Technical Report 062, Yale University, Department of Computer Science, 1976.

Uwagi

Opracowanie rekordu ze środków MEiN, umowa nr SONP/SP/546092/2022 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2022-2023). (PL)