Abstract
We present KReach, a tool for deciding reachability in general Petri nets. The tool is a full implementation of Kosaraju’s original 1982 decision procedure for reachability in VASS. We believe this to be the first implementation of its kind. We include a comprehensive suite of libraries for development with Vector Addition Systems (with States) in the Haskell programming language. KReach serves as a practical tool, and acts as an effective teaching aid for the theory behind the algorithm. Preliminary tests suggest that there are some classes of Petri nets for which we can quickly show unreachability. In particular, using KReach for coverability problems, by reduction to reachability, is competitive even against state-of-the-art coverability checkers.
Supported by the Centre for Doctoral Training in Urban Science and Progress (EPSRC Grant EP/L016400/1).
Chapter PDF
Similar content being viewed by others
References
Control.Concurrent - Haskell Package Database. http://hackage.haskell.org/package/base-4.12.0.0/docs/Control-Concurrent.html
Mist - a safety checker for Petri nets (and monotonic extensions). https://github.com/pierreganty/mist
Angeli, D., De Leenheer, P., Sontag, E.D.: Persistence results for chemical reaction networks with time-dependent kinetics and no global conservation laws. SIAM Journal on Applied Mathematics 71(1), 128–146 (2011). https://doi.org/10.1137/090779401
Blondin, M., Finkel, A., Haase, C., Haddad, S.: Approaching the coverability problem continuously. In: TACAS. LNCS, vol. 9636, pp. 480–496. Springer (2016). https://doi.org/10.1007/978-3-662-49674-9_28
Bouajjani, A., Emmi, M.: Analysis of recursively parallel programs. ACM Trans. Program. Lang. Syst. 35(3) (Nov 2013). https://doi.org/10.1145/2518188
Burns, F., Koelmans, A., Yakovlev, A.: WCET analysis of Superscalar Processors using Simulation with coloured Petri nets. Real-Time Systems 18, 275–288 (2000). https://doi.org/10.1023/A:1008101416758
Czerwinski, W., Lasota, S., Lazic, R., Leroux, J., Mazowiecki, F.: The reachability problem for Petri nets is not elementary. In: STOC. pp. 24–33. ACM (2019). https://doi.org/10.1145/3313276.3316369
Demri, S., Figueira, D., Praveen, M.: Reasoning about data repetitions with counter systems. Logical Methods in Computer Science 12(3) (2016). https://doi.org/10.2168/LMCS-12(3:1)2016
Esparza, J., Ganty, P., Leroux, J., Majumdar, R.: Verification of population protocols. Acta Inf. 54(2), 191–215 (2017). https://doi.org/10.1007/s00236-016-0272-3
Finkel, A., Haddad, S., Khmelnitsky, I.: Minimal coverability tree construction made complete and efficient. In: FoSSaCS (2020), https://hal.inria.fr/hal-02479879
Geffroy, T., Leroux, J., Sutre, G.: Occam’s razor applied to the petri net coverability problem. Theor. Comput. Sci. 750, 38–52 (2018). https://doi.org/10.1016/j.tcs.2018.04.014
Greibach, S.A.: Remarks on blind and partially blind one-way multicounter machines. Theor. Comput. Sci. 7, 311–324 (1978). https://doi.org/10.1016/0304-3975(78)90020-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 (swat 1974). pp. 156–164 (Oct 1974). https://doi.org/10.1109/SWAT.1974.28
Hopcroft, J.E., Pansiot, J.: On the reachability problem for 5-dimensional vector addition systems. Theor. Comput. Sci. 8, 135–159 (1979). https://doi.org/10.1016/0304-3975(79)90041-0
Kanovich, M.I.: Petri nets, Horn programs, linear logic and vector games. Ann. Pure Appl. Logic 75(1–2), 107–135 (1995). https://doi.org/10.1016/0168-0072(94)00060-G
Karp, R.M., Miller, R.E.: Parallel program schemata. J. Comput. Syst. Sci. 3(2), 147–195 (1969). https://doi.org/10.1016/S0022-0000(69)80011-5
Kosaraju, S.R.: Decidability of reachability in vector addition systems (preliminary version). In: STOC. pp. 267–281. ACM (1982). https://doi.org/10.1145/800070.802201
Lambert, J.: A structure to decide reachability in Petri nets. Theor. Comput. Sci. 99(1), 79–104 (1992). https://doi.org/10.1016/0304-3975(92)90173-D
Lasota, S.: VASS reachability in three steps. CoRR abs/1812.11966 (2018), http://arxiv.org/abs/1812.11966
Leroux, J.: The general vector addition system reachability problem by Presburger inductive invariants. Logical Methods in Computer Science 6(3) (2010). https://doi.org/10.2168/LMCS-6(3:22)2010
Leroux, J., Schmitz, S.: Reachability in vector addition systems is primitive-recursive in fixed dimension. In: LICS. pp. 1–13. IEEE (2019). https://doi.org/10.1109/LICS.2019.8785796
Li, Y., Deutsch, A., Vianu, V.: VERIFAS: A practical verifier for artifact systems. PVLDB 11(3), 283–296 (2017). https://doi.org/10.14778/3157794.3157798
Lipton, R.J.: The reachability problem requires exponential space. Tech. Rep. 62, Yale University (1976), http://cpsc.yale.edu/sites/default/files/files/tr63.pdf
Mayr, E.W.: An algorithm for the general petri net reachability problem. SIAM J. Comput. 13(3), 441–460 (1984). https://doi.org/10.1137/0213029
Meyer, R.: A theory of structural stationarity in the pi-calculus. Acta Inf. 46(2), 87–137 (2009). https://doi.org/10.1007/s00236-009-0091-x
Petri, C.A.: Kommunikation mit Automaten. http://edoc.sub.uni-hamburg.de/informatik/volltexte/2011/160/ (1962), PhD thesis, Universität Hamburg
Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci. 6, 223–231 (1978). https://doi.org/10.1016/0304-3975(78)90036-1
Reutenauer, C.: The mathematics of Petri nets. Prentice Hall (1990), translated by Ian Craig
Reutenauer, C.: Aspects Mathématiques des Réseaux de Petri. Masson (1989)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Dixon, A., Lazić, R. (2020). KReach: A Tool for Reachability in Petri Nets. In: Biere, A., Parker, D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2020. Lecture Notes in Computer Science(), vol 12078. Springer, Cham. https://doi.org/10.1007/978-3-030-45190-5_22
Download citation
DOI: https://doi.org/10.1007/978-3-030-45190-5_22
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45189-9
Online ISBN: 978-3-030-45190-5
eBook Packages: Computer ScienceComputer Science (R0)