A lazy query scheme for reachability analysis in Petri nets. (English) Zbl 1489.68161

Buchs, Didier (ed.) et al., Application and theory of Petri nets and concurrency. 42nd international conference, PETRI NETS 2021, virtual event, June 23–25, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12734, 360-378 (2021).
Summary: 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.
For the entire collection see [Zbl 1482.68013].


68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
68W05 Nonnumerical algorithms


LoLA; Uppaal; Meddly
Full Text: DOI HAL


[1] 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)
[2] 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) · Zbl 1105.68350
[3] Bonet, B.; Haslum, P.; Hickmott, S.; Thiébaux, S., Directed unfolding of Petri nets. ToPNOC, 1, 1, 172-198 (2008) · Zbl 1171.68562
[4] Chatain, T., Paulevé, L.: Goal-driven unfolding of Petri nets. In: CONCUR, pp. 18:1-18:16 (2017)
[5] Couvreur, J.-M., Thierry-Mieg, Y.: Hierarchical decision diagrams to exploit model structure. In: Wang, F., (ed.) FORTE, pp. 443-457 (2005) · Zbl 1169.68502
[6] Esparza, J., Römer, S., Vogler, W.: An improvement of McMillan’s unfolding algorithm. In: TACAS, pp. 87-106 (1996)
[7] Holzmann, G.J., Peled, D.: An improvement in formal verification. In: FORTE, pp. 197-211 (1994)
[8] Jezequel, L., Lime, D.: Lazy reachability analysis in distributed systems. In: CONCUR, pp. 17:1-17:14 (2016)
[9] Jezequel, L., Lime, D.: Let’s be lazy, we have time - or, lazy reachability analysis for timed automata. In: FORMATS, pp. 247-263 (2017) · Zbl 1494.68182
[10] Kordon, F., et al.: Complete Results for the 2020 Edition of the Model Checking Contest, June 2020. http://mcc.lip6.fr/2020/results.php
[11] Kordon, F., MCC’2015 - the fifth model checking contest, ToPNOC, 11, 262-273 (2016)
[12] 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)
[13] Lambert, J-L, A structure to decide reachability in Petri nets, TCS, 99, 1, 79-104 (1992) · Zbl 0769.68104
[14] Lehmann, A., Lohmann, N., Wolf, K.: Stubborn sets for simple linear time properties. In: ICATPN, pp. 228-247 (2012)
[15] Leroux, J., Schmitz, S.: Demystifying reachability in vector addition systems. In: LICS, pp. 56-67. IEEE Computer Society (2015)
[16] 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)
[17] Mayr, EW, An algorithm for the general Petri net reachability problem, SIAM J. Comput., 13, 3, 441-460 (1984) · Zbl 0563.68057
[18] McMillan, K.: Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In: CAV, pp. 164-177 (1993)
[19] Miner, A., Babar, J.: Meddly: multi-terminal and edge-valued decision diagram library. In: QEST, pp. 195-196 (2010)
[20] Reinhardt, K., Reachability in Petri nets with inhibitor arcs, ENTCS, 223, 239-264 (2008) · Zbl 1337.68191
[21] Weiser, M.: Program slicing. IEEE Trans. Softw. Eng. SE-10(4), 352-357 (1984) · Zbl 0552.68004
[22] Wolf, K.: Running LoLA 2.0 in a model checking competition. ToPNOC 11, 274-285 (2016)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.