Skip to main content
SpringerLink
Log in

Coverability and Termination in Recursive Petri Nets

  • Conference paper
  • First Online:
Application and Theory of Petri Nets and Concurrency (PETRI NETS 2019)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,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.

A. Finkel—The work of this author was carried out in the framework of ReLaX, UMI2000 and also supported by ANR-17-CE40-0028 project BRAVAS.

S. Haddad—The work of this author was partly supported by ERC project EQualIS (FP7-308087).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  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. 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_16

    Chapter  Google Scholar 

  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)

    MathSciNet  MATH  Google Scholar 

  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. Dassow, J., Turaev, S.: Petri net controlled grammars: the case of special Petri nets. J. UCS 15(14), 2808–2835 (2009)

    MathSciNet  MATH  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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. Finkel, A., Haddad, S., Khmelnitsky, I.: Coverability and termination in recursive Petri nets, April 2019. https://hal.inria.fr/hal-02081019

  9. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theor. Comput. Sci. 256(1–2), 63–92 (2001)

    Article  MathSciNet  Google Scholar 

  10. Haddad, S., Poitrenaud, D.: Decidability and undecidability results for recursive Petri nets. Technical Report 019, LIP6, Paris VI University (1999)

    Google Scholar 

  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_14

    Chapter  MATH  Google Scholar 

  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_48

    Chapter  MATH  Google Scholar 

  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. Haddad, S., Poitrenaud, D.: Recursive Petri nets. Acta Inf. 44(7–8), 463–508 (2007)

    Article  Google Scholar 

  15. Lambert, J.-L.: A structure to decide reachability in Petri nets. Theor. Comput. Sci. 99(1), 79–104 (1992)

    Article  MathSciNet  Google Scholar 

  16. Lazic, R.: The reachability problem for vector addition systems with a stack is not elementary. CoRR, abs/1310.1767 (2013)

    Google Scholar 

  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. 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. Lipton, R.J.: The reachability problem requires exponential space. Technical Report 062, Yale University, Department of Computer Science, January 1976

    Google Scholar 

  20. Mavlankulov, G., Othman, M., Turaev, S., Selamat, M.H., Zhumabayeva, L., Zhukabayeva, T.: Concurrently controlled grammars. Kybernetika 54(4), 748–764 (2018)

    MathSciNet  MATH  Google Scholar 

  21. Mayr, E.W.: An algorithm for the general Petri net reachability problem. SIAM J. Comput. 13(3), 441–460 (1984)

    Article  MathSciNet  Google Scholar 

  22. Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci. 6(2), 223–231 (1978)

    Article  MathSciNet  Google Scholar 

  23. Reinhardt, K.: Reachability in Petri nets with inhibitor arcs. Electr. Notes Theor. Comput. Sci. 223, 239–264 (2008)

    Article  Google Scholar 

  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_54

    Chapter  Google Scholar 

  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_15

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LSV, ENS Paris-Saclay, CNRS, Université Paris-Saclay, Cachan, France

    Alain Finkel, Serge Haddad & Igor Khmelnitsky

  2. Inria, Paris, France

    Serge Haddad & Igor Khmelnitsky

Authors
  1. Alain Finkel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Serge Haddad
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Igor Khmelnitsky
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Igor Khmelnitsky .

Editor information

Editors and Affiliations

  1. Università di Torino, Turin, Italy

    Susanna Donatelli

  2. Inria and LSV, CNRS & ENS Paris-Saclay, Cachan Cedex, France

    Stefan Haar

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Finkel, A., Haddad, S., Khmelnitsky, I. (2019). Coverability and Termination in Recursive Petri Nets. In: Donatelli, S., Haar, S. (eds) Application and Theory of Petri Nets and Concurrency. PETRI NETS 2019. Lecture Notes in Computer Science(), vol 11522. Springer, Cham. https://doi.org/10.1007/978-3-030-21571-2_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-21571-2_23

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-21570-5

  • Online ISBN: 978-3-030-21571-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation