Symbolic and Structural Model-Checking

• Autorzy: Thierry-Mieg Yann

Identyfikatory

DOI

10.3233/FI-2021-2090

• Języki publikacji: EN

Abstrakty

EN

Brute-force model-checking consists in exhaustive exploration of the state-space of a Petri net, and meets the dreaded state-space explosion problem. In contrast, this paper shows how to solve model-checking problems using a combination of techniques that stay in complexity proportional to the size of the net structure rather than to the state-space size. We combine an SMT based over-approximation to prove that some behaviors are unfeasible, an under-approximation using memory-less sampling of runs to find witness traces or counter-examples, and a set of structural reduction rules that can simplify both the system and the property. This approach was able to win by a clear margin the model-checking contest 2020 for reachability queries as well as deadlock detection, thus demonstrating the practical effectiveness and general applicability of the system of rules presented in this paper.

Słowa kluczowe

EN

Petri nets; structural reduction; model-checking; SMT constraints

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2021
• Tom: Vol. 183, nr 3-4
• Strony: 319--342
• Opis fizyczny: Bibliogr. 20 poz.

Twórcy

autor

Thierry-Mieg Yann

• Sorbonne Université, CNRS, LIP6, F-75005 Paris, France

Bibliografia

• [1] de Moura LM, Bjørner N. Z3: An Efficient SMT Solver. In: TACAS, volume 4963 of Lecture Notes in
• Computer Science. Springer, 2008 pp. 337-340. doi:10.1007/978-3-540-78800-3_24.
• [2] Wimmel H, Wolf K. Applying CEGAR to the Petri Net State Equation. In: TACAS, volume 6605 of Lecture Notes in Computer Science. Springer, 2011 pp. 224-238. doi:10.2168/LMCS-8(3:27)2012.
• [3] Clarke EM, Grumberg O, Jha S, Lu Y, Veith H. Counterexample-Guided Abstraction Refinement. In: CAV, volume 1855 of LNCS. Springer, 2000 pp. 154-169. doi:10.1007/10722167_15.
• [4] Lipton RJ. Reduction: A Method of Proving Properties of Parallel Programs. Commun. ACM, 1975. 18(12):717-721. doi:10.1145/361227.361234.
• [5] Berthelot G. Checking properties of nets using transformation. In: Applications and Theory in Petri Nets, volume 222 of Lecture Notes in Computer Science. Springer, 1985 pp. 19-40.
• [6] Thierry-Mieg Y. Structural Reductions Revisited. In: Petri Nets, volume 12152 of Lecture Notes in Computer Science. Springer, 2020 pp. 303-323. doi:10.1007/978-3-030-51831-8_15.
• [7] Amparore EG, Berthomieu B, Ciardo G, Dal-Zilio S, Gallà F, Hillah L, Hulin-Hubard F, Jensen PG, Jezequel L, Kordon F, Botlan DL, Liebke T, Meijer J, Miner AS, Paviot-Adet E, Srba J, Thierry-Mieg Y, van Dijk T, Wolf K. Presentation of the 9th Edition of the Model Checking Contest. In: Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III, volume 11429 of Lecture Notes in Computer Science. Springer, 2019 pp. 50-68. doi:10.1007/978-3-030-17502-3_4.
• [8] D’Anna M, Trigila S. Concurrent system analysis using Petri nets: an optimized algorithm for finding net invariants. Computer Communications, 1988. 11(4):215-220. doi:10.1016/0140-3664(88)90085-0.
• [9] Best E, Schlachter U. Analysis of Petri Nets and Transition Systems. In: ICE, volume 189 of EPTCS. 2015 pp. 53-67. doi:10.4204/EPTCS.189.6.
• [10] 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.
• [11] Murata T. State equation, controllability, and maximal matchings of Petri nets. IEEE Transactions on Automatic Control, 1977. 22:412-416.
• [12] Laarman A. Stubborn Transaction Reduction. In: NFM, volume 10811 of Lecture Notes in Computer Science. Springer, 2018 pp. 280-298. doi:10.1007/978-3-319-77935-5_20.
• [13] Evangelista S, Haddad S, Pradat-Peyre J. Syntactical Colored Petri Nets Reductions. In: ATVA, volume 3707 of Lecture Notes in Computer Science. Springer, 2005 pp. 202-216. doi:10.1007/11562948_17.
• [14] Haddad S, Pradat-Peyre J. New Efficient Petri Nets Reductions for Parallel Programs Verification. Parallel Processing Letters, 2006. 16(1):101-116. doi:10.1142/S0129626406002502.
• [15] Bønneland FM, Dyhr J, Jensen PG, Johannsen M, Srba J. Stubborn versus structural reductions for Petr I nets. J. Log. Algebr. Meth. Program., 2019. 102:46-63. doi:10.1016/j.jlamp.2018.09.002.
• [16] Berthomieu B, Le Botlan D, Dal Zilio S. Counting Petri net markings from reduction equations. International Journal on Software Tools for Technology Transfer, 2019. 22:163-181. doi:10.1007/s10009-019-00519-1.
• [17] Liu G, Barkaoui K. A survey of siphons in Petri nets. Inf. Sci., 2016. 363:198-220. doi:10.1016/j.ins.2015.08.037.
• [18] García-Vallés F, Colom JM. Implicit places in net systems. In: PNPM. IEEE Computer Society, 1999 pp. 104-113. doi:10.1109/PNPM.1999.796557.
• [19] Bønneland F, Dyhr J, Jensen PG, Johannsen M, Srba J. Simplification of CTL Formulae for Efficient Model Checking of Petri Nets. In: Petri Nets, volume 10877 of Lecture Notes in Computer Science. Springer, 2018 pp. 143-163. doi:10.1007/978-3-319-91268-4_8.
• [20] Thierry-Mieg Y. Symbolic Model-Checking Using ITS-Tools. In: TACAS, volume 9035 of Lecture Notes in Computer Science. Springer, 2015 pp. 231-237. doi:10.1007/978-3-662-46681-0_20.

Uwagi

Opracowanie rekordu ze środków MEiN, umowa nr SONP/SP/546092/2022 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2022-2023). (PL)