Computing Parameterized Invariants of Parameterized Petri Nets

• Autorzy: Esparza Javier , Raskin Mikhail , Welzel Christoph

Identyfikatory

DOI

10.3233/FI-222137

• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

parameterized systems; logic; theorem proving; first-order; WS1S

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2022
• Tom: vol. 187 nr 2-4
• Strony: 197--243
• Opis fizyczny: Bibliogr. 60 poz., rys., tab.

Twórcy

autor

Esparza Javier

• Department of Informatics Technical University of Munich Munich, Germany

autor

Raskin Mikhail

• Department of Informatics Technical University of Munich Munich, Germany

autor

Welzel Christoph

• Department of Informatics Technical University of Munich Munich, Germany

Bibliografia

• [1] Murata T. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 1989. 77(4):541-580.
• [2] Reisig W. Understanding Petri Nets - Modeling Techniques, Analysis Methods, Case Studies. Springer, 2013. ISBN:978-3-642-33277-7.
• [3] Desel J, Esparza J. Free choice Petri nets. Cambridge university press, 2005. ISBN-10:0521019451, 13:978-0521019453.
• [4] Bensalem S, Bozga M, Nguyen T, Sifakis J. D-Finder: A Tool for Compositional Deadlock Detection and Verification. In: CAV, volume 5643 of LNCS. 2009 pp. 614-619. doi:10.1007/978-3-642-02658-4 45.
• [5] Esparza J, Ledesma-Garza R, Majumdar R, Meyer PJ, Niksic F. An SMT-Based Approach to Coverability Analysis. In: CAV, volume 8559 of LNCS. Springer, 2014 pp. 603-619. doi:10.1007/978-3-319-08867-9 40.
• [6] Blondin M, Finkel A, Haase C, Haddad S. Approaching the Coverability Problem Continuously. In: TACAS, volume 9636 of LNCS. Springer, 2016 pp. 480-496. doi:10.1007/978-3-662-49674-9 28.
• [7] Wimmel H, Wolf K. Applying CEGAR to the Petri Net State Equation. Logical Methods in Computer Science, 2012. 8(3). doi:10.1007/978-3-642-19835-9 19.
• [8] Bozga M, Iosif R, Sifakis J. Checking Deadlock-Freedom of Parametric Component-Based Systems. In: TACAS (2), volume 11428 of LNCS. Springer, 2019 pp. 3-20. doi:10.48550/arXiv.1805.10073.
• [9] Bozga M, Esparza J, Iosif R, Sifakis J, Welzel C. Structural Invariants for the Verification of Systems with Parameterized Architectures. In: TACAS (1), volume 12078 of LNCS. Springer, 2020 pp. 228-246. doi:10.1007/978-3-030-45190-5 13.
• [10] Bloem R, Jacobs S, Khalimov A, Konnov I, Rubin S, Veith H, Widder J. Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2015. doi:10.1007/978-3-031-02011-7.
• [11] Esparza J. Parameterized Verification of Crowds of Anonymous Processes. In: Dependable Software Systems Engineering, IOS Press, 2016 pp. 59-71. doi:10.3233/978-1-61499-627-9-59.
• [12] Abdulla PA, Sistla AP, Talupur M. Model Checking Parameterized Systems. In: Handbook of Model Checking, pp. 685-725. Springer, 2018. doi:10.1007/978-3-319-10575-8 21.
• [13] The MONA Project. MONA. URL https://www.bricks.dk/mona.
• [14] Henriksen JG, Jensen JL, Jørgensen ME, Klarlund N, Paige R, Rauhe T, Sandholm A. MONA: Monadic Second-Order Logic in Practice. In: TACAS, volume 1019 of LNCS. Springer, 1995 pp. 89-110.
• [15] Apt KR, Kozen DC. Limits for automatic verification of finite-state concurrent systems. Information Processing Letters, 1986. 22(6):307 - 309.
• [16] Esparza J, Melzer S. Verification of Safety Properties Using Integer Programming: Beyond the State Equation. Formal Methods in System Design, 2000. 16(2):159-189. doi:10.1023/A:1008743212620.
• [17] Esparza J, Meyer PJ. An SMT-based Approach to Fair Termination Analysis. In: FMCAD. IEEE, 2015 pp. 49-56. doi:10.1109/FMCAD.2015.7542252.
• [18] Blondin M, Esparza J, Helfrich M, Kucera A, Meyer PJ. Checking Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling. In: CAV (2), volume 12225 of LNCS. Springer, 2020 pp. 372-397. doi:10.1007/978-3-030-53291-8 20.
• [19] German SM, Sistla AP. Reasoning about Systems with Many Processes. J. ACM, 1992. 39(3):675-735.
• [20] Abdulla PA, Cerans K, Jonsson B, Tsay Y. General Decidability Theorems for Infinite-State Systems. In: LICS. IEEE Computer Society, 1996 pp. 313-321.
• [21] Finkel A, Schnoebelen P. Well-structured transition systems everywhere! Theor. Comput. Sci., 2001. 256(1-2):63-92. doi:10.1016/S0304-3975(00)00102-X.
• [22] Blondin M, Finkel A, Haase C, Haddad S. Approaching the Coverability Problem Continuously. In: TACAS, volume 9636 of LNCS. Springer, 2016 pp. 480-496. doi:10.1007/978-3-662-49674-9 28.
• [23] Geffroy T, Leroux J, Sutre G. Occam’s Razor applied to the Petri net coverability problem. Theor. Comput. Sci., 2018. 750:38-52. doi:10.1016/j.tcs.2018.04.014.
• [24] Reynier P, Servais F. On the Computation of the Minimal Coverability Set of Petri Nets. In: RP, volume 11674 of LNCS. Springer, 2019 pp. 164-177. doi:10.1007/978-3-030-30806-3 13.
• [25] Finkel A, Haddad S, Khmelnitsky I. Minimal Coverability Tree Construction Made Complete and Efficient. In: FoSSaCS, volume 12077 of LNCS. Springer, 2020 pp. 237-256. doi:10.1007/978-3-030-45231-5 13.
• [26] Athanasiou K, Liu P, Wahl T. Unbounded-Thread Program Verification using Thread-State Equations. In: IJCAR, volume 9706 of LNCS. Springer, 2016 pp. 516-531. doi:10.1007/978-3-319-40229-1 35.
• [27] Kesten Y, Maler O, Marcus M, Pnueli A, Shahar E. Symbolic model checking with rich assertional languages. Theor. Comput. Sci, 2001. 256(1-2):93 - 112. doi:10.1016/S0304-3975(00)00103-1.
• [28] Abdulla PA, Jonsson B, Nilsson M, Saksena M. A Survey of Regular Model Checking. In: CONCUR, volume 3170 of LNCS. Springer, 2004 pp. 35-48. doi:10.1007/978-3-540-28644-8 3.
• [29] Abdulla PA, Delzanno G, Henda NB, Rezine A. Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems). In: TACAS, volume 4424 of LNCS. Springer, 2007 pp. 721-736. doi:10.1007/978-3-540-71209-1 56.
• [30] Baukus K, Bensalem S, Lakhnech Y, Stahl K. Abstracting WS1S Systems to Verify Parameterized Networks. In: TACAS, volume 1785 of LNCS. Springer, 2000 pp. 188-203. doi:10.1007/3-540-46419-0 14.
• [31] Baukus K, Lakhnech Y, Stahl K. Parameterized Verification of a Cache Coherence Protocol: Safety and Liveness. In: VMCAI, volume 2294 of LNCS. Springer, 2002 pp. 317-330. doi:10.1007/3-540-47813-2 22.
• [32] Chen Y, Hong C, Lin AW, R¨ummer P. Learning to prove safety over parameterised concurrent systems. In: FMCAD. 2017 pp. 76-83. doi:10.23919/FMCAD.2017.8102244.
• [33] Browne M, Clarke E, Grumberg O. Reasoning about networks with many identical finite state processes. Information and Computation, 1989. 81(1):13 - 31.
• [34] Emerson EA, Namjoshi KS. Reasoning about Rings. In: POPL. 1995 pp. 85-94.
• [35] Emerson EA, Kahlon V. Reducing Model Checking of the Many to the Few. In: CADE, volume 1831 of LNCS. Springer, 2000 pp. 236-254. doi:10.1007/10721959 19.
• [36] Außerlechner S, Jacobs S, Khalimov A. Tight Cutoffs for Guarded Protocols with Fairness. In: VMCAI, volume 9583 of LNCS. Springer, 2016 pp. 476-494. doi:10.1007/978-3-662-49122-5 23.
• [37] Jacobs S, Sakr M. Analyzing Guarded Protocols: Better Cutoffs, More Systems, More Expressivity. In: VMCAI, volume 10747 of LNCS. Springer, 2018 pp. 247-268. doi:10.1007/978-3-319-73721-8 12.
• [38] Esparza J. Decidability and Complexity of Petri Net Problems - An Introduction. In: Petri Nets, volume 1491 of Lecture Notes in Computer Science. Springer, 1996 pp. 374-428. doi:10.1007/3-540-65306-6 20.
• [39] Esparza J, Raskin M, Welzel C. Computing Parameterized Invariants of Parameterized Petri Nets, 2021. 2103.10280, URL https://arxiv.org/abs/2103.10280.
• [40] Esparza J, Finkel A, Mayr R. On the Verification of Broadcast Protocols. In: LICS. IEEE Computer Society, 1999 pp. 352-359.
• [41] Delzanno G. Automatic Verification of Parameterized Cache Coherence Protocols. In: CAV. 2000 pp. 53-68. doi:10.1007/10722167 8.
• [42] Dijkstra EW. Cooperating Sequential Processes, pp. 65-138. Springer New York, New York, NY. ISBN:978-1-4757-3472-0, 2002. doi:10.1007/978-1-4757-3472-02.
• [43] Lynch NA. Distributed Algorithms. Morgan Kaufmann, 1996.
• [44] Herlihy M, Shavit N. The art of multiprocessor programming. Morgan Kaufmann, 2008.
• [45] Welzel C, Esparza J, Raskin M. ostrich, 2020. doi:10.5281/zenodo.6523828.
• [46] Fribourg L, Ols´en H. Reachability sets of parameterized rings as regular languages. Electr. Notes Theor. Comput. Sci., 1997. 9:40. doi:10.1016/S1571-0661(05)80427-X.
• [47] Jensen HE, Lynch NA. A Proof of Burns N-Process Mutual Exclusion Algorithm Using Abstraction. In: TACAS, volume 1384 of Lecture Notes in Computer Science. Springer, 1998 pp. 409-423.
• [48] Esparza J, Raskin M, Welzel C. heron, git repository. https://gitlab.lrz.de/i7/heron, 2021.
• [49] Welzel C, Esparza J, Raskin M. heron, software artifact. https://doi.org/10.5281/zenodo.5068849, 2020. doi:10.5281/zenodo.5068849.
• [50] Gebser M, Kaufmann B, Kaminski R, Ostrowski M, Schaub T, Schneider M. Potassco: The Potsdam Answer Set Solving Collection. AI Commun., 2011. 24(2):107-124. doi:10.3233/AIC-2011-0491.
• [51] Kov´acs L, Voronkov A. First-Order Theorem Proving and Vampire. In: CAV, volume 8044 of Lecture Notes in Computer Science. Springer, 2013 pp. 1-35. doi:10.1007/978-3-642-39799-8 1.
• [52] Barrett CW, Conway CL, Deters M, Hadarean L, Jovanovic D, King T, Reynolds A, Tinelli C. CVC4. In: CAV, volume 6806 of Lecture Notes in Computer Science. Springer, 2011 pp. 171-177. doi:10.1007/978-3-642-22110-1 14.
• [53] Knuth DE. Additional comments on a problem in concurrent programming control. Commun. ACM, 1966. 9(5):321-322. doi:10.1145/363162.363167.
• [54] de Bruijn NG. Additional comments on a problem in concurrent programming control. Commun. ACM, 1967. 10(3):137-138. doi:10.1145/355592.365595.
• [55] Eisenberg MA, McGuire MR. Further Comments on Dijkstra’s Concurrent Programming Control Problem. Commun. ACM, 1972. 15(11):999. doi:10.1145/355606.361895.
• [56] Szymanski BK. Mutual exclusion revisited. In: Next Decade in Information Technology: Proceedings of the 5th Jerusalem Conference on Information Technology 1990, Jerusalem, October 22-25, 1990. 1990 pp. 110-117. doi:10.1109/JCIT.1990.128275.
• [57] Bouajjani A, Jonsson B, Nilsson M, Touili T. Regular Model Checking. In: CAV. 2000 pp. 403-418. doi:10.1007/10722167 31.
• [58] Esparza J, Raskin M, Welzel C. ostrich. https://gitlab.lrz.de/i7/ostrich, 2021.
• [59] Esparza J, Raskin MA, Welzel C. Computing Parameterized Invariants of Parameterized Petri Nets. In: Petri Nets, volume 12734 of Lecture Notes in Computer Science. Springer, 2021 pp. 141-163. doi:10.1007/978-3-030-76983-3 8.
• [60] Esparza J, Raskin MA, Welzel C. Abduction of trap invariants in parameterized systems. In: GandALF, volume 346 of EPTCS. 2021 pp. 1-17. doi:10.4204/EPTCS.346.1.