Abstract
Numerous tasks in program analysis and synthesis reduce to deciding reachability in possibly infinite graphs such as those induced by Petri nets. However, the Petri net reachability problem has recently been shown to require non-elementary time, which raises questions about the practical applicability of Petri nets as target models. In this paper, we introduce a novel approach for efficiently semi-deciding the reachability problem for Petri nets in practice. Our key insight is that computationally lightweight over-approximations of Petri nets can be used as distance oracles in classical graph exploration algorithms such as \(\mathsf {A}^{*}\) and greedy best-first search. We provide and evaluate a prototype implementation of our approach that outperforms existing state-of-the-art tools, sometimes by orders of magnitude, and which is also competitive with domain-specific tools on benchmarks coming from program synthesis and concurrent program analysis.
An extended version containing full proofs as well as a primer on applications of the Petri net reachability problem can be obtained from: arxiv.org/abs/2010.07912.
This work is part of a project that has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (Grant agreement No. 852769, ARiAT). It is also supported by a Discovery Grant from the Natural Sciences and Engineering Research Council of Canada (NSERC). Parts of this research were carried out while the second author was affiliated with the Department of Computer Science, University College London, UK.
Chapter PDF
Similar content being viewed by others
References
Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.: General decidability theorems for infinite-state systems. In: Proc. \(\text{11}^\text{th }\) Annual IEEE Symposium on Logic in Computer Science (LICS). pp. 313–321. IEEE Computer Society (1996). https://doi.org/10.1109/LICS.1996.561359
Angeli, D., De Leenheer, P., Sontag, E.D.: A Petri net approach to the study of persistence in chemical reaction networks. Mathematical Biosciences 210(2), 598–618 (2007). https://doi.org/10.1016/j.mbs.2007.07.003
Araki, T., Kasami, T.: Some decision problems related to the reachability problem for Petri nets. Theoretical Computer Science 3(1), 85–104 (1976). https://doi.org/10.1016/0304-3975(76)90067-0
Athanasiou, K., Liu, P., Wahl, T.: Unbounded-thread program verification using thread-state equations. In: Proc. \({{8}^{\rm th}}\) International Joint Conference on Automated Reasoning (IJCAR). pp. 516–531. Springer (2016). https://doi.org/10.1007/978-3-319-40229-1_35
Bansal, K., Koskinen, E., Wies, T., Zufferey, D.: Structural counter abstraction. In: Proc. \({{19}^{{\rm th}}}\) International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pp. 62–77. Springer (2013). https://doi.org/10.1007/978-3-642-36742-7_5
Barth, A., Mitchell, J.C., Datta, A., Sundaram, S.: Privacy and utility in business processes. In: Proc. \({{20}^{\rm th}}\) IEEE Computer Security Foundations Symposium (CSF). pp. 279–294. IEEE Computer Society (2007). https://doi.org/10.1109/CSF.2007.26
Bjørner, N., Phan, A., Fleckenstein, L.: \(\nu \)Z - an optimizing SMT solver. In: Proc. \({{21}^{\rm th}}\) International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pp. 194–199. Springer (2015). https://doi.org/10.1007/978-3-662-46681-0_14
Blondin, M., Finkel, A., Haase, C., Haddad, S.: The logical view on continuous Petri nets. ACM Transactions on Computational Logic (TOCL) 18(3), 24:1–24:28 (2017). https://doi.org/10.1145/3105908
Blondin, M., Haase, C., Mazowiecki, F.: Affine extensions of integer vector addition systems with states. In: Proc. \({{29}^{\rm th}}\) International Conference on Concurrency Theory (CONCUR). pp. 14:1–14:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2018). https://doi.org/10.4230/LIPIcs.CONCUR.2018.14
Blondin, M., Haase, C., Offtermatt, P.: Fastforward: A tool for reachability in Petri nets with infinite state spaces. Artifact for the TACAS21 contribution “Directed Reachability for Infinite-State Systems” (2021). https://doi.org/10.6084/m9.figshare.13573592
Chaouiya, C.: Petri net modelling of biological networks. Briefings in Bioinformatics 8(4), 210–219 (2007). https://doi.org/10.1093/bib/bbm029
Chistikov, D., Haase, C., Halfon, S.: Context-free commutative grammars with integer counters and resets. Theoretical Computer Science 735, 147–161 (2018). https://doi.org/10.1016/j.tcs.2016.06.017
Czerwiński, W., Lasota, S., Lazić, R., Leroux, J., Mazowiecki, F.: The reachability problem for Petri nets is not elementary. In: Proc. \({{51}^{\rm st}}\) Annual ACM SIGACT Symposium on Theory of Computing (STOC). pp. 24–33. ACM (2019). https://doi.org/10.1145/3313276.3316369
David, R., Alla, H.: Continuous Petri nets. In: Proc. \({{8}^{\rm th}}\) European Workshop on Application and Theory of Petri nets. vol. 340, pp. 275–294 (1987)
David, R., Alla, H.: Discrete, Continuous, and Hybrid Petri nets. Springer, \({{2}^{\rm nd}}\) edn. (2010)
Delzanno, G., Raskin, J., Van Begin, L.: Towards the automated verification of multithreaded Java programs. In: Proc. \({{8}^{\rm th}}\) International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pp. 173–187. Springer (2002). https://doi.org/10.1007/3-540-46002-0_13
Dixon, A., Lazić, R.: Kreach: A tool for reachability in Petri nets. In: Proc. \({{26}^{\rm th}}\) International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pp. 405–412. Springer (2020). https://doi.org/10.1007/978-3-030-45190-5_22
D’Osualdo, E., Kochems, J., Ong, C.L.: Automatic verification of erlang-style concurrency. In: Proc. \({{20}^{\rm th}}\) International Symposium on Static Analysis (SAS). pp. 454–476. Springer (2013). https://doi.org/10.1007/978-3-642-38856-9_24
Dufourd, C., Finkel, A., Schnoebelen, P.: Reset nets between decidability and undecidability. In: Proc. \({{25}^{\rm th}}\) International Colloquium on Automata, Languages and Programming (ICALP). pp. 103–115. Springer (1998). https://doi.org/10.1007/BFb0055044
Edelkamp, S., Schuppan, V., Bosnacki, D., Wijs, A., Fehnker, A., Aljazzar, H.: Survey on directed model checking. In: Proc. \({{5}^{\rm th}}\) International Workshop on Model Checking and Artificial Intelligence (MoChArt). pp. 65–89. Springer (2008). https://doi.org/10.1007/978-3-642-00431-5_5
Esparza, J.: Decidability and complexity of Petri net problems — An introduction, pp. 374–428. Springer (1998). https://doi.org/10.1007/3-540-65306-6_20
Esparza, J., Ganty, P., Leroux, J., Majumdar, R.: Verification of population protocols. Acta Informatica 54(2), 191–215 (2017). https://doi.org/10.1007/s00236-016-0272-3
Esparza, J., Ledesma-Garza, R., Majumdar, R., Meyer, P.J., Nikšić, F.: An SMT-based approach to coverability analysis. In: Proc. \({{26}^{\rm th}}\) International Conference on Computer Aided Verification (CAV). pp. 603–619. Springer (2014). https://doi.org/10.1007/978-3-319-08867-9_40
Feng, Y., Martins, R., Wang, Y., Dillig, I., Reps, T.W.: Component-based synthesis for complex APIs. In: Proc. \({{44}^{\rm th}}\) ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). pp. 599–612. ACM (2017). https://doi.org/10.1145/3009837.3009851
Fraca, E., Haddad, S.: Complexity analysis of continuous Petri nets. Fundamenta Informaticae 137(1), 1–28 (2015). https://doi.org/10.3233/FI-2015-1168
Galenson, J.: Dynamic and Interactive Synthesis of Code Snippets. Ph.D. thesis, University of California (2014)
Galenson, J., Reames, P., Bodík, R., Hartmann, B., Sen, K.: Codehint: dynamic and interactive synthesis of code snippets. In: Proc. \({{36}^{\rm th}}\) International Conference on Software Engineering (ICSE). pp. 653–663. ACM (2014). https://doi.org/10.1145/2568225.2568250
Ganty, P.: Algorithmes et structures de données efficaces pour la manipulation de contraintes sur les intervalles. Master’s thesis, Université Libre de Bruxelles (2002), (In French)
Geffroy, T., Leroux, J., Sutre, G.: Occam’s razor applied to the Petri net coverability problem. Theoretical Computer Science 750, 38–52 (2018). https://doi.org/10.1016/j.tcs.2018.04.014
German, S.M., Sistla, A.P.: Reasoning about systems with many processes. Journal of the ACM 39(3), 675–735 (1992). https://doi.org/10.1145/146637.146681
Gupta, U., Shah, P., Akshay, S., Hofman, P.: Continuous reachability for unordered data Petri nets is in PTime. In: Proc. \({{22}^{\rm nd}}\) International Conference on Foundations of Software Science and Computation Structures (FoSSaCS). pp. 260–276. Springer (2019). https://doi.org/10.1007/978-3-030-17127-8_15
Gurobi Optimization, L.: Gurobi optimizer reference manual (2020), http://www.gurobi.com
Heiner, M., Gilbert, D.R., Donaldson, R.: Petri nets for systems and synthetic biology. In: Formal Methods for Computational Systems Biology. pp. 215–264. Springer (2008). https://doi.org/10.1007/978-3-540-68894-5_7
Hofman, P., Leroux, J., Totzke, P.: Linear combinations of unordered data vectors. In: Proc. \({{32}^{\rm nd}}\) Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). pp. 1–11. IEEE Computer Society (2017). https://doi.org/10.1109/LICS.2017.8005065
Janák, J.: Issue Tracking Systems. Master’s thesis, Masaryk University (2009)
Jeng, M.D., Chen, S.C.: A heuristic search approach using approximate solutions to Petri net state equations for scheduling flexible manufacturing systems. International Journal of Flexible Manufacturing Systems 10(2), 139–162 (1998). https://doi.org/10.1023/A:1008097430956
Jensen, K.: Coloured Petri nets: basic concepts, analysis methods and practical use, vol. 1. Springer Science & Business Media (2013)
Jones, N.D., Landweber, L.H., Lien, Y.E.: Complexity of some problems in Petri nets. Theoretical Computer Science 4(3), 277–299 (1977). https://doi.org/10.1016/0304-3975(77)90014-7
Kaiser, A., Kroening, D., Wahl, T.: A widening approach to multithreaded program verification. ACM Transactions on Programming Languages and Systems (TOPLAS) 36(4), 14:1–14:29 (2014). https://doi.org/10.1145/2629608
Kosaraju, S.R.: Decidability of reachability in vector addition systems (preliminary version). In: Proc. \({{14}^{\rm th}}\) Symposium on Theory of Computing (STOC). pp. 267–281. ACM (1982). https://doi.org/10.1145/800070.802201
Lambert, J.: A structure to decide reachability in Petri nets. Theoretical Computer Science 99(1), 79–104 (1992). https://doi.org/10.1016/0304-3975(92)90173-D
Lee, D.Y., DiCesare, F.: Scheduling flexible manufacturing systems using Petri nets and heuristic search. IEEE Transactions on robotics and automation 10(2), 123–132 (1994). https://doi.org/10.1109/70.282537
Leroux, J.: Vector addition systems reachability problem (A simpler solution). In: Turing-100 - The Alan Turing Centenary. pp. 214–228. EasyChair (2012).
Leroux, J., Schmitz, S.: Demystifying reachability in vector addition systems. In: Proc. \({{30}^{\rm th}}\) Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). pp. 56–67. IEEE Computer Society (2015). https://doi.org/10.1109/LICS.2015.16
Lipton, R.J.: The reachability problem requires exponential space. Tech. rep., Yale University (1976)
Liu, B., Dong, W., Zhang, Y.: Accelerating API-based program synthesis via API usage pattern mining. IEEE Access 7, 159162–159176 (2019). https://doi.org/10.1109/ACCESS.2019.2950232
Mayr, E.W.: An algorithm for the general Petri net reachability problem. In: Proc. \({{13}^{\rm th}}\) Symposium on Theory of Computing (STOC). pp. 238–246. ACM (1981). https://doi.org/10.1145/800076.802477
Mejía, G., Odrey, N.G.: An approach using Petri nets and improved heuristic search for manufacturing system scheduling. Journal of Manufacturing Systems 24(2), 79–92 (2005). https://doi.org/10.1016/S0278-6125(05)80009-3
de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: Proc. \({{14}^{\rm th}}\) International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). pp. 337–340. Springer (2008). https://doi.org/10.1007/978-3-540-78800-3_24, tool available at https://github.com/Z3Prover/z3.
Murata, T.: Petri nets: Properties, analysis and applications. Proceedings of the IEEE 77(4), 541–580 (1989). https://doi.org/10.1109/5.24143
Rackoff, C.: The covering and boundedness problems for vector addition systems. Theoretical Computer Science 6, 223–231 (1978). https://doi.org/10.1016/0304-3975(78)90036-1
Russell, S., Norvig, P.: Artificial Intelligence: A Modern Approach. Prentice Hall Press, \({{3}^{\rm rd}}\) edn. (2009)
Schmidt, K.: LoLA: A low level analyser. In: Proc. International Conference on Application and Theory of Petri Nets (ICATPN). pp. 465–474. Springer (2000). https://doi.org/10.1007/3-540-44988-4_27
Silverman, J., Kincaid, Z.: Loop summarization with rational vector addition systems. In: Proc. \({{31}^{\rm st}}\) International Conference on Computer Aided Verification (CAV). pp. 97–115. Springer (2019). https://doi.org/10.1007/978-3-030-25543-5_7
Strazny, T.: An algorithmic framework for checking coverability in well-structured transition systems. Ph.D. thesis, Universität Oldenburg (2014), http://csd.informatik.uni-oldenburg.de/~skript/pub/diss/strazny-phdthesis-roterbericht.pdf
Uma, G., Prasad, B.: Reachability trees for Petri nets: a heuristic approach. Knowledge-Based Systems 6(3), 174 – 177 (1993). https://doi.org/10.1016/0950-7051(93)90042-R
van der Aalst, W.: The application of Petri nets to workflow management. Journal of Circuits, Systems, and Computers 8(1), 21–66 (1998). https://doi.org/10.1142/S0218126698000043
Watel, D., Weisser, M., Barth, D.: Parameterized complexity and approximability of coverability problems in weighted Petri nets. In: Proc. \({{38}^{\rm th}}\) International Conference on Application and Theory of Petri Nets and Concurrency (PETRI NETS). pp. 330–349. Springer (2017). https://doi.org/10.1007/978-3-319-57861-3_19
Wynn, M.T., van der Aalst, W.M.P., ter Hofstede, A.H.M., Edmond, D.: Synchronization and cancelation in workflows based on reset nets. International Journal of Cooperative Information Systems 18(1), 63–114 (2009). https://doi.org/10.1142/S0218843009002002
Yang, C.H., Dill, D.L.: Validation with guided search of the state space. In: Proc. \({{35}^{\rm th}}\) Conference on Design Automation (DAC). pp. 599–604. ACM (1998). https://doi.org/10.1145/277044.277201
Zuck, L.D., Pnueli, A.: Model checking and abstraction to the aid of parameterized systems (a survey). Computer Languages, Systems & Structures 30(3-4), 139–169 (2004). https://doi.org/10.1016/j.cl.2004.02.006
Acknowledgments
We thank Juliette Fournis d’Albiat for her help with extracting the sypet suite.
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
© 2021 The Author(s)
About this paper
Cite this paper
Blondin, M., Haase, C., Offtermatt, P. (2021). Directed Reachability for Infinite-State Systems. In: Groote, J.F., Larsen, K.G. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2021. Lecture Notes in Computer Science(), vol 12652. Springer, Cham. https://doi.org/10.1007/978-3-030-72013-1_1
Download citation
DOI: https://doi.org/10.1007/978-3-030-72013-1_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-72012-4
Online ISBN: 978-3-030-72013-1
eBook Packages: Computer ScienceComputer Science (R0)