Abstract
In recent works we proposed a lazy algorithm for reachability analysis in networks of automata. This algorithm is optimistic and tries to take into account as few automata as possible to perform its task. In this paper we extend the approach to the more general settings of reachability analysis in unbounded Petri nets and reachability analysis in bounded Petri nets with inhibitor arcs. We consider we are given a reachability algorithm and we organize queries to it on bigger and bigger nets in a lazy manner, trying thus to consider as few places and transitions as possible to make a decision. Our approach has been implemented in the Romeo model checker and tested on benchmarks from the model checking contest.
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
Notes
- 1.
It uses the classical list data structure. The length of a list L is given by length(L). The \(k^{th}\) element of L is L[k].
- 2.
64bits Linux binaries for Romeo and converters from pnml (MCC) to cts (Romeo), and full results are at http://lara.rts-software.org/.
References
Akshay, S., Chakraborty, S., Das, A., Jagannath, V., Sandeep, S.: On Petri nets with hierarchical special arcs. In: CONCUR, pp. 40:1–40:17 (2017)
Behrmann, G., David, A., Larsen, K.G.: A tutorial on UPPAAL. In: International School on Formal Methods for the Design of Computer, Communication and Software Systems, pp. 200–236 (2004)
Bonet, B., Haslum, P., Hickmott, S., Thiébaux, S.: Directed unfolding of Petri nets. ToPNOC 1(1), 172–198 (2008)
Chatain, T., Paulevé, L.: Goal-driven unfolding of Petri nets. In: CONCUR, pp. 18:1–18:16 (2017)
Couvreur, J.-M., Thierry-Mieg, Y.: Hierarchical decision diagrams to exploit model structure. In: Wang, F., (ed.) FORTE, pp. 443–457 (2005)
Esparza, J., Römer, S., Vogler, W.: An improvement of McMillan’s unfolding algorithm. In: TACAS, pp. 87–106 (1996)
Holzmann, G.J., Peled, D.: An improvement in formal verification. In: FORTE, pp. 197–211 (1994)
Jezequel, L., Lime, D.: Lazy reachability analysis in distributed systems. In: CONCUR, pp. 17:1–17:14 (2016)
Jezequel, L., Lime, D.: Let’s be lazy, we have time - or, lazy reachability analysis for timed automata. In: FORMATS, pp. 247–263 (2017)
Kordon, F., et al.: Complete Results for the 2020 Edition of the Model Checking Contest, June 2020. http://mcc.lip6.fr/2020/results.php
Kordon, F., et al.: MCC’2015 - the fifth model checking contest. ToPNOC 11, 262–273 (2016)
Rao Kosaraju, S.: Decidability of reachability in vector addition systems (preliminary version). In: Lewis, H.R., Simons, B.B., Burkhard, W.A., Landweber, L.H. (eds.) STOC, pp. 267–281. ACM (1982)
Lambert, J.-L.: A structure to decide reachability in Petri nets. TCS 99(1), 79–104 (1992)
Lehmann, A., Lohmann, N., Wolf, K.: Stubborn sets for simple linear time properties. In: ICATPN, pp. 228–247 (2012)
Leroux, J., Schmitz, S.: Demystifying reachability in vector addition systems. In: LICS, pp. 56–67. IEEE Computer Society (2015)
Lime, D., Roux, O.H., Seidner, C., Traonouez, L.-M.: Romeo: a parametric model-checker for Petri nets with stopwatches. In: TACAS, pp. 54–57 (2009)
Mayr, E.W.: An algorithm for the general Petri net reachability problem. SIAM J. Comput. 13(3), 441–460 (1984)
McMillan, K.: Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In: CAV, pp. 164–177 (1993)
Miner, A., Babar, J.: Meddly: multi-terminal and edge-valued decision diagram library. In: QEST, pp. 195–196 (2010)
Reinhardt, K.: Reachability in Petri nets with inhibitor arcs. ENTCS 223, 239–264 (2008)
Weiser, M.: Program slicing. IEEE Trans. Softw. Eng. SE-10(4), 352–357 (1984)
Wolf, K.: Running LoLA 2.0 in a model checking competition. ToPNOC 11, 274–285 (2016)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Jezequel, L., Lime, D., Sérée, B. (2021). A Lazy Query Scheme for Reachability Analysis in Petri Nets. In: Buchs, D., Carmona, J. (eds) Application and Theory of Petri Nets and Concurrency. PETRI NETS 2021. Lecture Notes in Computer Science(), vol 12734. Springer, Cham. https://doi.org/10.1007/978-3-030-76983-3_18
Download citation
DOI: https://doi.org/10.1007/978-3-030-76983-3_18
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-76982-6
Online ISBN: 978-3-030-76983-3
eBook Packages: Computer ScienceComputer Science (R0)