Advertisement

Coverability and Termination in Recursive Petri Nets

  • Alain Finkel
  • Serge Haddad
  • Igor KhmelnitskyEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11522)

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.

Keywords

Recursive Petri nets Expressiveness Complexity Coverability Termination 

References

  1. 1.
    Atig, M.F., Ganty, P.: Approximating Petri net reachability along context-free traces. In: FSTTCS 2011, Mumbai, India, LIPIcs, vol. 13, pp. 152–163 (2011)Google Scholar
  2. 2.
    Bonnet, R.: The reachability problem for vector addition system with one zero-test. In: Murlak, F., Sankowski, P. (eds.) MFCS 2011. LNCS, vol. 6907, pp. 145–157. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22993-0_16CrossRefGoogle Scholar
  3. 3.
    Bonnet, R., Finkel, A., Leroux, J., Zeitoun, M.: Model checking vector addition systems with one zero-test. Logical Methods Comput. Sci. 8(11), 1–25 (2012)MathSciNetzbMATHGoogle Scholar
  4. 4.
    Czerwinski, W., Lasota, S., Lazic, R., Leroux, J., Mazowiecki, F.: The reachability problem for Petri nets is not elementary (extended abstract). CoRR, abs/1809.07115 (2018)Google Scholar
  5. 5.
    Dassow, J., Turaev, S.: Petri net controlled grammars: the case of special Petri nets. J. UCS 15(14), 2808–2835 (2009)MathSciNetzbMATHGoogle Scholar
  6. 6.
    Demri, S., Jurdziński, M., Lachish, O., Lazić, R.: The covering and boundedness problems for branching vector addition systems. J. Comput. Syst. Sci. 79(1), 23–38 (2012)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Fallah Seghrouchni, A.E., Haddad, S.: A recursive model for distributed planning. In: ICMAS 1996, Kyoto, Japan, pp. 307–314 (1996)Google Scholar
  8. 8.
    Finkel, A., Haddad, S., Khmelnitsky, I.: Coverability and termination in recursive Petri nets, April 2019. https://hal.inria.fr/hal-02081019
  9. 9.
    Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theor. Comput. Sci. 256(1–2), 63–92 (2001)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Haddad, S., Poitrenaud, D.: Decidability and undecidability results for recursive Petri nets. Technical Report 019, LIP6, Paris VI University (1999)Google Scholar
  11. 11.
    Haddad, S., Poitrenaud, D.: Theoretical aspects of recursive Petri nets. In: Donatelli, S., Kleijn, J. (eds.) ICATPN 1999. LNCS, vol. 1639, pp. 228–247. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48745-X_14CrossRefzbMATHGoogle Scholar
  12. 12.
    Haddad, S., Poitrenaud, D.: Modelling and analyzing systems with recursive Petri nets. In: Boel, R., Stremersch, G. (eds.) Discrete Event Systems. The International Series in Engineering and Computer Science, vol. 569, pp. 449–458. Springer, Boston (2000).  https://doi.org/10.1007/978-1-4615-4493-7_48CrossRefzbMATHGoogle Scholar
  13. 13.
    Haddad, S., Poitrenaud, D.: Checking linear temporal formulas on sequential recursive Petri nets. In: TIME 2001, Civdale del Friuli, Italy, pp. 198–205. IEEE Computer Society (2001)Google Scholar
  14. 14.
    Haddad, S., Poitrenaud, D.: Recursive Petri nets. Acta Inf. 44(7–8), 463–508 (2007)CrossRefGoogle Scholar
  15. 15.
    Lambert, J.-L.: A structure to decide reachability in Petri nets. Theor. Comput. Sci. 99(1), 79–104 (1992)MathSciNetCrossRefGoogle Scholar
  16. 16.
    Lazic, R.: The reachability problem for vector addition systems with a stack is not elementary. CoRR, abs/1310.1767 (2013)Google Scholar
  17. 17.
    Lazic,R., Schmitz, S.: Non-elementary complexities for branching vass, mell, and extensions. In: CSL-LICS 2014, Vienna, Austria, pp. 61:1–61:10. ACM (2014)Google Scholar
  18. 18.
    Lazić, R., Schmitz,S.: The complexity of coverability in \(\nu \)-Petri nets. In: LICS 2016, pp. 467–476. ACM Press, New York (2016)Google Scholar
  19. 19.
    Lipton, R.J.: The reachability problem requires exponential space. Technical Report 062, Yale University, Department of Computer Science, January 1976Google Scholar
  20. 20.
    Mavlankulov, G., Othman, M., Turaev, S., Selamat, M.H., Zhumabayeva, L., Zhukabayeva, T.: Concurrently controlled grammars. Kybernetika 54(4), 748–764 (2018)MathSciNetzbMATHGoogle Scholar
  21. 21.
    Mayr, E.W.: An algorithm for the general Petri net reachability problem. SIAM J. Comput. 13(3), 441–460 (1984)MathSciNetCrossRefGoogle Scholar
  22. 22.
    Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci. 6(2), 223–231 (1978)MathSciNetCrossRefGoogle Scholar
  23. 23.
    Reinhardt, K.: Reachability in Petri nets with inhibitor arcs. Electr. Notes Theor. Comput. Sci. 223, 239–264 (2008)CrossRefGoogle Scholar
  24. 24.
    Schnoebelen, P.: Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets. In: Hliněný, P., Kučera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 616–628. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15155-2_54CrossRefGoogle Scholar
  25. 25.
    Zetzsche, G.: The emptiness problem for valence automata or: another decidable extension of Petri nets. In: Bojańczyk, M., Lasota, S., Potapov, I. (eds.) RP 2015. LNCS, vol. 9328, pp. 166–178. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-24537-9_15CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Alain Finkel
    • 1
  • Serge Haddad
    • 1
    • 2
  • Igor Khmelnitsky
    • 1
    • 2
    Email author
  1. 1.LSV, ENS Paris-Saclay, CNRS, Université Paris-SaclayCachanFrance
  2. 2.InriaParisFrance

Personalised recommendations