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 to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
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
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
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
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
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
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
Ginsburg, S., Spanier, E.H.: Semigroups, presburger formulas, and languages. Pacific J. Math. 16(2), 285–296 (1966)
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
Hack, M.: Decidability Questions for Petri Nets. Outstanding Dissertations in the Computer Sciences. Garland Publishing, New York (1975)
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
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
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
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
Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci. 6, 223–231 (1978)
Reisig, W.: Understanding Petri Nets (Modeling Techniques, Analysis Methods, Case Studies). Springer, Heidelberg (2013). 230 pp
Wimmel, H.: Entscheidbarkeit bei Petri Netzen: Überblick und Kompendium. Springer, Heidelberg (2008). 242 pp
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
Corresponding author
Editor information
Editors and Affiliations
Rights 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)