×

Computing parameterized invariants of parameterized Petri nets. (English) Zbl 1489.68158

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, 141-163 (2021).
Summary: A fundamental advantage of Petri net models is the possibility to automatically compute useful system invariants from the syntax of the net. Classical techniques used for this are place invariants, P-components, siphons or traps. Recently, Bozga et al. have presented a novel technique for the parameterized verification of safety properties of systems with a ring or array architecture. They show that the statement “for every instance of the parameterized Petri net, all markings satisfying the linear invariants associated to all the P-components, siphons and traps of the instance are safe” can be encoded in WS1S and checked using tools like MONA. However, while the technique certifies that this infinite set of linear invariants extracted from P-components, siphons or traps are strong enough to prove safety, it does not return an explanation of this fact understandable by humans. We present a CEGAR loop that constructs a finite set of parameterized P-components, siphons or traps, whose infinitely many instances are strong enough to prove safety. For this we design parameterization procedures for different architectures.
For the entire collection see [Zbl 1482.68013].

MSC:

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

Software:

MONA; D-Finder
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Abdulla, P.A., Cerans, K., Jonsson, B., Tsay, Y.: General decidability theorems for infinite-state systems. In: LICS, pp. 313-321. IEEE Computer Society (1996)
[2] Abdulla, PA; Delzanno, G.; Henda, NB; Rezine, A.; Grumberg, O.; Huth, M., Regular model checking without transducers (on efficient verification of parameterized systems), Tools and Algorithms for the Construction and Analysis of Systems, 721-736 (2007), Heidelberg: Springer, Heidelberg · Zbl 1186.68312 · doi:10.1007/978-3-540-71209-1_56
[3] Abdulla, PA; Jonsson, B.; Nilsson, M.; Saksena, M.; Gardner, P.; Yoshida, N., A survey of regular model checking, CONCUR 2004 - Concurrency Theory, 35-48 (2004), Heidelberg: Springer, Heidelberg · Zbl 1099.68055 · doi:10.1007/978-3-540-28644-8_3
[4] Abdulla, PA; Sistla, AP; Talupur, M., Model checking parameterized systems, Handbook of Model Checking, 685-725 (2018), Cham: Springer, Cham · Zbl 1392.68223 · doi:10.1007/978-3-319-10575-8_21
[5] Apt, KR; Kozen, DC, Limits for automatic verification of finite-state concurrent systems, Inf. Process. Lett., 22, 6, 307-309 (1986) · doi:10.1016/0020-0190(86)90071-2
[6] Athanasiou, K.; Liu, P.; Wahl, T.; Olivetti, N.; Tiwari, A., Unbounded-thread program verification using thread-state equations, Automated Reasoning, 516-531 (2016), Cham: Springer, Cham · Zbl 1475.68174 · doi:10.1007/978-3-319-40229-1_35
[7] Außerlechner, S.; Jacobs, S.; Khalimov, A.; Jobstmann, B.; Leino, KRM, Tight cutoffs for guarded protocols with fairness, Verification, Model Checking, and Abstract Interpretation, 476-494 (2016), Heidelberg: Springer, Heidelberg · Zbl 1475.68175 · doi:10.1007/978-3-662-49122-5_23
[8] Baukus, K.; Bensalem, S.; Lakhnech, Y.; Stahl, K.; Graf, S.; Schwartzbach, M., Abstracting WS1S systems to verify parameterized networks, Tools and Algorithms for the Construction and Analysis of Systems, 188-203 (2000), Heidelberg: Springer, Heidelberg · Zbl 0964.68096 · doi:10.1007/3-540-46419-0_14
[9] Baukus, K.; Lakhnech, Y.; Stahl, K.; Cortesi, A., Parameterized verification of a cache coherence protocol: safety and liveness, Verification, Model Checking, and Abstract Interpretation, 317-330 (2002), Heidelberg: Springer, Heidelberg · Zbl 1057.68620 · doi:10.1007/3-540-47813-2_22
[10] Bensalem, S.; Bozga, M.; Nguyen, T-H; Sifakis, J.; Bouajjani, A.; Maler, O., D-finder: a tool for compositional deadlock detection and verification, Computer Aided Verification, 614-619 (2009), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-02658-4_45
[11] Bloem, R., Decidability of parameterized verification, Synth. Lect. Distrib. Comput. Theory, 6, 1-170 (2015) · Zbl 1400.68006 · doi:10.2200/S00658ED1V01Y201508DCT013
[12] Blondin, M.; Esparza, J.; Helfrich, M.; Kučera, A.; Meyer, PJ; Lahiri, SK; Wang, C., Checking qualitative liveness properties of replicated systems with stochastic scheduling, Computer Aided Verification, 372-397 (2020), Cham: Springer, Cham · Zbl 1478.68147 · doi:10.1007/978-3-030-53291-8_20
[13] Blondin, M.; Finkel, A.; Haase, C.; Haddad, S.; Chechik, M.; Raskin, J-F, Approaching the coverability problem continuously, Tools and Algorithms for the Construction and Analysis of Systems, 480-496 (2016), Heidelberg: Springer, Heidelberg · Zbl 1420.68144 · doi:10.1007/978-3-662-49674-9_28
[14] Bozga, M.; Esparza, J.; Iosif, R.; Sifakis, J.; Welzel, C., Structural invariants for the verification of systems with parameterized architectures, Tools and Algorithms for the Construction and Analysis of Systems, 228-246 (2020), Cham: Springer, Cham · Zbl 1507.68179 · doi:10.1007/978-3-030-45190-5_13
[15] Bozga, M.; Iosif, R.; Sifakis, J.; Vojnar, T.; Zhang, L., Checking deadlock-freedom of parametric component-based systems, Tools and Algorithms for the Construction and Analysis of Systems, 3-20 (2019), Cham: Springer, Cham · Zbl 1527.68022 · doi:10.1007/978-3-030-17465-1_1
[16] Browne, M.; Clarke, E.; Grumberg, O., Reasoning about networks with many identical finite state processes, Inf. Comput., 81, 1, 13-31 (1989) · Zbl 0709.68610 · doi:10.1016/0890-5401(89)90026-6
[17] Chen, Y., Hong, C., Lin, A.W., Rümmer, P.: Learning to prove safety over parameterised concurrent systems. In: FMCAD, pp. 76-83 (2017)
[18] Delzanno, G.: Automatic verification of parameterized cache coherence protocols. In: CAV, pp. 53-68 (2000). doi:10.1007/10722167_8 · Zbl 0974.68500
[19] Desel, J.; Esparza, J., Free Choice Petri Nets (2005), Cambridge: Cambridge University Press, Cambridge · Zbl 0836.68074
[20] Dijkstra, E.W.: Cooperating sequential processes. In: Hansen, P.B. (ed.) The Origin of Concurrent Programming, pp. 65-138. Springer, New York (2002). doi:10.1007/978-1-4757-3472-02
[21] Emerson, EA; Kahlon, V.; McAllester, D., Reducing model checking of the many to the few, Automated Deduction - CADE-17, 236-254 (2000), Heidelberg: Springer, Heidelberg · Zbl 0963.68109 · doi:10.1007/10721959_19
[22] Emerson, E.A., Namjoshi, K.S.: Reasoning about rings. In: POPL, pp. 85-94 (1995)
[23] Esparza, J.; Reisig, W.; Rozenberg, G., Decidability and complexity of petri net problems—an introduction, Lectures on Petri Nets I: Basic Models, 374-428 (1998), Heidelberg: Springer, Heidelberg · Zbl 0926.68087 · doi:10.1007/3-540-65306-6_20
[24] Esparza, J.: Parameterized verification of crowds of anonymous processes. In: Dependable Software Systems Engineering, pp. 59-71. IOS Press (2016)
[25] Esparza, J., Finkel, A., Mayr, R.: On the verification of broadcast protocols. In: LICS, pp. 352-359. IEEE Computer Society (1999)
[26] Esparza, J.; Ledesma-Garza, R.; Majumdar, R.; Meyer, P.; Niksic, F.; Biere, A.; Bloem, R., An SMT-based approach to coverability analysis, Computer Aided Verification, 603-619 (2014), Cham: Springer, Cham · Zbl 1487.68156 · doi:10.1007/978-3-319-08867-9_40
[27] Esparza, J.; Melzer, S., Verification of safety properties using integer programming: beyond the state equation, Formal Methods Syst. Des., 16, 2, 159-189 (2000) · doi:10.1023/A:1008743212620
[28] Esparza, J., Meyer, P.J.: An SMT-based approach to fair termination analysis. In: FMCAD, pp. 49-56. IEEE (2015)
[29] Esparza, J., Raskin, M., Welzel, C.: Computing parameterized invariants of parameterized petri nets (2021). https://arxiv.org/abs/2103.10280
[30] Esparza, J., Raskin, M., Welzel, C.: Computing parameterized invariants of parameterized petri nets (2021). https://gitlab.lrz.de/i7/ostrich · Zbl 1489.68158
[31] Finkel, A.; Haddad, S.; Khmelnitsky, I., Minimal coverability tree construction made complete and efficient, Foundations of Software Science and Computation Structures, 237-256 (2020), Cham: Springer, Cham · Zbl 07250941 · doi:10.1007/978-3-030-45231-5_13
[32] Finkel, A.; Schnoebelen, P., Well-structured transition systems everywhere!, Theor. Comput. Sci., 256, 1-2, 63-92 (2001) · Zbl 0973.68170 · doi:10.1016/S0304-3975(00)00102-X
[33] Fribourg, L.; Olsén, H., Reachability sets of parameterized rings as regular languages, Electr. Notes Theor. Comput. Sci., 9, 40 (1997) · Zbl 0907.68119 · doi:10.1016/S1571-0661(05)80427-X
[34] Geffroy, T.; Leroux, J.; Sutre, G., Occam’s razor applied to the petri net coverability problem, Theor. Comput. Sci., 750, 38-52 (2018) · Zbl 1402.68134 · doi:10.1016/j.tcs.2018.04.014
[35] German, SM; Sistla, AP, Reasoning about systems with many processes, J. ACM, 39, 3, 675-735 (1992) · Zbl 0799.68078 · doi:10.1145/146637.146681
[36] Henriksen, JG; Brinksma, E.; Cleaveland, WR; Larsen, KG; Margaria, T.; Steffen, B., Mona: monadic second-order logic in practice, Tools and Algorithms for the Construction and Analysis of Systems, 89-110 (1995), Heidelberg: Springer, Heidelberg · doi:10.1007/3-540-60630-0_5
[37] Jacobs, S.; Sakr, M., Analyzing guarded protocols: better cutoffs, more systems, more expressivity, Verification, Model Checking, and Abstract Interpretation, 247-268 (2018), Cham: Springer, Cham · Zbl 1446.68105 · doi:10.1007/978-3-319-73721-8_12
[38] Jensen, HE; Lynch, NA; Steffen, B., A proof of burns \(N\)-process mutual exclusion algorithm using abstraction, Tools and Algorithms for the Construction and Analysis of Systems, 409-423 (1998), Heidelberg: Springer, Heidelberg · doi:10.1007/BFb0054186
[39] Kesten, Y.; Maler, O.; Marcus, M.; Pnueli, A.; Shahar, E., Symbolic model checking with rich assertional languages, Theor. Comput. Sci, 256, 1, 93-112 (2001) · Zbl 0973.68119 · doi:10.1016/S0304-3975(00)00103-1
[40] Murata, T., Petri nets: properties, analysis and applications, Proc. IEEE, 77, 4, 541-580 (1989) · doi:10.1109/5.24143
[41] Reisig, W., Understanding Petri Nets - Modeling Techniques, Analysis Methods, Case Studies (2013), Heidelberg: Springer, Heidelberg · Zbl 1278.68222 · doi:10.1007/978-3-642-33278-4
[42] Reynier, P-A; Servais, F.; Filiot, E.; Jungers, R.; Potapov, I., On the computation of the minimal coverability set of petri nets, Reachability Problems, 164-177 (2019), Cham: Springer, Cham · Zbl 07121144 · doi:10.1007/978-3-030-30806-3_13
[43] The MONA Project: MONA. https://www.bricks.dk/mona
[44] Welzel, C., Esparza, J., Raskin, M.: Ostrich (2020). doi:10.5281/zenodo.4499091
[45] Wimmel, H., Wolf, K.: Applying CEGAR to the Petri net state equation. Log. Methods Comput. Sci 8(3), (2012) · Zbl 1248.68360
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.