Skip to main content
SpringerLink
Log in
Book cover

International Conference on Current Trends in Theory and Practice of Informatics

SOFSEM 2017: SOFSEM 2017: Theory and Practice of Computer Science pp 91–102Cite as

Deciding Structural Liveness of Petri Nets

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10139))

Abstract

Place/transition Petri nets are a standard model for a class of distributed systems whose reachability spaces might be infinite. One of well-studied topics is the verification of safety and liveness properties in this model; despite the extensive research effort, some basic problems remain open, which is exemplified by the open complexity status of the reachability problem. The liveness problems are known to be closely related to the reachability problem, and many structural properties of nets that are related to liveness have been studied.

Somewhat surprisingly, the decidability status of the problem if a net is structurally live, i.e. if there is an initial marking for which it is live, has remained open, as also a recent paper (Best and Esparza, 2016) emphasizes. Here we show that the structural liveness problem for Petri nets is decidable.

A crucial ingredient of the proof is the result by Leroux (LiCS 2013) showing that we can compute a finite (Presburger) description of the reachability set for a marked Petri net if this set is semilinear.

Supported by the Grant Agency of the Czech Rep., project GAČR:15-13784S.

This is a preview of subscription content, 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

Learn about institutional subscriptions

References

  1. Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.: Algorithmic analysis of programs with well quasi-ordered domains. Inf. Comput. 160(1–2), 109–127 (2000). http://dx.doi.org/10.1006/inco.1999.2843

    Article  MathSciNet  MATH  Google Scholar 

  2. Barkaoui, K., Pradat-Peyre, J.: On liveness and controlled siphons in Petri nets. Application and Theory of Petri Nets 1996. LNCS, vol. 1091, pp. 57–72. Springer, Heidelberg (1996). doi:10.1007/3-540-61363-3_4

    Chapter  Google Scholar 

  3. Best, E., Esparza, J.: Existence of home states in Petri nets is decidable. Inf. Process. Lett. 116(6), 423–427 (2016). http://dx.doi.org/10.1016/j.ipl.2016.01.011

    Article  MathSciNet  MATH  Google Scholar 

  4. Esparza, J.: Decidability and complexity of Petri net problems—an introduction. In: Reisig, W., Rozenberg, G. (eds.) ACPN 1996. LNCS, vol. 1491, pp. 374–428. Springer, Heidelberg (1998). doi:10.1007/3-540-65306-6_20

    Chapter  Google Scholar 

  5. Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, Part II: complete WSTS. Logical Methods Comput. Sci. 8(3) (2012). http://dx.doi.org/10.2168/LMCS-8(3:28)2012

  6. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theor. Comput. Sci. 256(1–2), 63–92 (2001). http://dx.doi.org/10.1016/S0304-3975(00)00102-X

    Article  MathSciNet  MATH  Google Scholar 

  7. Ginsburg, S., Spanier, E.H.: Semigroups, presburger formulas, and languages. Pacific J. Math. 16(2), 285–296 (1966)

    Article  MathSciNet  MATH  Google Scholar 

  8. Hack, M.: The recursive equivalence of the reachability problem and the liveness problem for Petri nets and vector addition systems. In: 15th Annual Symposium on Switching and Automata Theory, New Orleans, Louisiana, USA, October 14–16, 1974, pp. 156–164. IEEE Computer Society (1974). http://dx.doi.org/10.1109/SWAT.1974.28

  9. Hack, M.: Decidability Questions for Petri Nets. Outstanding Dissertations in the Computer Sciences. Garland Publishing, New York (1975)

    Google Scholar 

  10. Leroux, J.: Vector addition systems reachability problem (A simpler solution). In: Voronkov, A. (ed.) Turing-100 - The Alan Turing Centenary, Manchester, UK, June 22–25, 2012. EPiC Series in Computing, vol. 10, pp. 214–228. EasyChair (2012). http://www.easychair.org/publications/?page=1673703727

  11. Leroux, J.: Presburger vector addition systems. In: 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25–28, 2013, pp. 23–32. IEEE Computer Society (2013). http://dx.doi.org/10.1109/LICS.2013.7

  12. Leroux, J., Schmitz, S.: Demystifying reachability in vector addition systems. In: 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6–10, 2015, pp. 56–67. IEEE Computer Society (2015). http://dx.doi.org/10.1109/LICS.2015.16

  13. Mayr, E.W.: An algorithm for the general petri net reachability problem. SIAM J. Comput. 13(3), 441–460 (1984). http://dx.doi.org/10.1137/0213029

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  15. Reisig, W.: Understanding Petri Nets (Modeling Techniques, Analysis Methods, Case Studies). Springer, Heidelberg (2013). 230 pp

    Book  MATH  Google Scholar 

  16. Wimmel, H.: Entscheidbarkeit bei Petri Netzen: Überblick und Kompendium. Springer, Heidelberg (2008). 242 pp

    Google Scholar 

Download references

Acknowledgement

I would like to thank Eike Best for drawing my attention to the problem of structural liveness studied in this paper. I also thank the anonymous reviewers for helpful comments.

Author information

Authors and Affiliations

  1. Department of Computer Science, FEI, Technical University, Ostrava, Czech Republic

    Petr Jančar

Authors
  1. Petr Jančar
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Petr Jančar .

Editor information

Editors and Affiliations

  1. TU Dortmund , Dortmund, Germany

    Bernhard Steffen

  2. TU Dresden , Dresden, Germany

    Christel Baier

  3. Eindhoven University of Technology , Eindhoven, The Netherlands

    Mark van den Brand

  4. Alpen Adria University Klagenfurt , Klagenfurt, Austria

    Johann Eder

  5. Lero - Irish Software Research Center , Limerick, Ireland

    Mike Hinchey

  6. Lero - Irish Software Research Center , Limerick, Ireland

    Tiziana Margaria

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Jančar, P. (2017). Deciding Structural Liveness of Petri Nets. In: Steffen, B., Baier, C., van den Brand, M., Eder, J., Hinchey, M., Margaria, T. (eds) SOFSEM 2017: Theory and Practice of Computer Science. SOFSEM 2017. Lecture Notes in Computer Science(), vol 10139. Springer, Cham. https://doi.org/10.1007/978-3-319-51963-0_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-51963-0_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-51962-3

  • Online ISBN: 978-3-319-51963-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation