A Polyhedral Abstraction for Petri Nets and its Application to SMT-Based Model Checking

• Autorzy: Amat Nicolas , Berthomieu Bernard , Dal Zilio Silvano

Identyfikatory

DOI

10.3233/FI-222134

• Języki publikacji: EN

Abstrakty

EN

We define a new method for taking advantage of net reductions in combination with a SMT-based model checker. Our approach consists in transforming a reachability problem about some Petri net, into the verification of an updated reachability property on a reduced version of this net. This method relies on a new state space abstraction based on systems of constraints, called polyhedral abstraction. We prove the correctness of this method using a new notion of equivalence between nets. We provide a complete framework to define and check the correctness of equivalence judgements; prove that this relation is a congruence; and give examples of basic equivalence relations that derive from structural reductions. Our approach has been implemented in a tool, named SMPT, that provides two main procedures: Bounded Model Checking (BMC) and Property Directed Reachability (PDR). Each procedure has been adapted in order to use reductions and to work with arbitrary Petri nets. We tested SMPT on a large collection of queries used in the Model Checking Contest. Our experimental results show that our approach works well, even when we only have a moderate amount of reductions.

Słowa kluczowe

EN

Computer Science - Logic in Computer Science

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

Twórcy

autor

Amat Nicolas

• LAAS-CNRS Universit´e de Toulouse, CNRS, INSA, Toulouse, France

autor

Berthomieu Bernard

• LAAS-CNRS Universit´e de Toulouse, CNRS, Toulouse, France

autor

Dal Zilio Silvano

• LAAS-CNRS Universit´e de Toulouse, CNRS, Toulouse, France

Bibliografia

• [1] Berthelot G. Transformations and Decompositions of Nets. In: Petri Nets: Central Models and their Properties, volume 254 of LNCS. Springer, 1987 doi:10.1007/978-3-540-47919-2 13.
• [2] Berthomieu B, Le Botlan D, Dal Zilio S. Petri net reductions for counting markings. In: Model Checking Software (SPIN), volume 10869 of LNCS. Springer, 2018 doi:10.1007/978-3-319-94111-0 4.
• [3] 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. doi:10.1007/s10009-019-00519-1.
• [4] Thierry-Mieg Y, Poitrenaud D, Hamez A, Kordon F. Hierarchical set decision diagrams and regular models. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 5505 of LNCS. Springer, 2009 doi:10.1007/978-3-642-00768-2 1.
• [5] Amparore E, Berthomieu B, Ciardo G, Dal Zilio S, Gall`a F, Hillah LM, Hulin-Hubard F, Jensen PG, Jezequel L, Kordon F, Le Botlan D, Liebke T, Meijer J, Miner A, 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 (TACAS), volume 11429 of LNCS. Springer, 2019 doi:10.1007/978-3-662-58381-4 9.
• [6] Barrett C, Fontaine P, Tinelli C. The SMT-LIB Standard: Version 2.6. Technical report, Department of Computer Science, The University of Iowa, 2017. Available at http://www.smt-lib.org/.
• [7] Besson F, Jensen T, Talpin JP. Polyhedral analysis for synchronous languages. In: Static Analysis Symposium (SAS), volume 1694 of LNCS. Springer, 1999 doi:10.1007/3-540-48294-6 4.
• [8] Feautrier P. Automatic parallelization in the polytope model. In: The Data Parallel Programming Model, volume 1132 of LNCS. Springer, 1996. doi:10.1007/3-540-61736-1 44.
• [9] Biere A, Cimatti A, Clarke E, Zhu Y. Symbolic Model Checking without BDDs. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 1579 of LNCS. Springer, 1999 doi:10.1007/3-540-49059-0 14.
• [10] Bradley AR. SAT-Based Model Checking without Unrolling. In: Verification, Model Checking, and Abstract Interpretation (VMCAI), volume 6538 of LNCS. Springer, 2011. doi:10.1007/978-3-642-18275-47.
• [11] Bradley AR. Understanding IC3. In: Theory and Applications of Satisfiability Testing (SAT), volume 7317 of LNCS. Springer, 2012. doi:10.1007/978-3-642-31612-8 1.
• [12] Amat N, Berthomieu B, Dal Zilio S. On the Combination of Polyhedral Abstraction and SMT-Based Model Checking for Petri Nets. In: Application and Theory of Petri Nets and Concurrency (Petri Nets), volume 12734 of LNCS. Springer, 2021 doi:10.1007/978-3-030-76983-3 9.
• [13] Lloret JC, Az´ema P, Vernadat F. Compositional design and verification of communication protocols, using labelled Petri nets. In: Computer-Aided Verification (CAV), volume 531 of LNCS. Springer, Berlin, Heidelberg, 1991 doi:10.1007/BFb0023723.
• [14] Hujsa T, Berthomieu B, Dal Zilio S, Le Botlan D. Checking marking reachability with the state equation in Petri net subclasses. arXiv preprint arXiv:2006.05600, 2020.
• [15] Clarke E, Biere A, Raimi R, Zhu Y. Bounded Model Checking Using Satisfiability Solving. Formal Methods in System Design, 2001. 19. doi:10.1023/A:1011276507260.
• [16] Heljanko K. Bounded Reachability Checking with Process Semantics. In: International Conference on Concurrency Theory (CONCUR), volume 2154 of LNCS. Springer, 2001 doi:10.1007/3-540-44685-0 15.
• [17] Armando A, Mantovani J, Platania L. Bounded Model Checking of Software Using SMT Solvers Instead of SAT Solvers. In: Model Checking Software (SPIN), volume 3925 of LNCS. Springer, 2006 doi:10.1007/11691617 9.
• [18] Cimatti A, Griggio A, Mover S, Tonetta S. Infinite-state invariant checking with IC3 and predicate abstraction. Formal Methods in System Design, 2016. 49. doi:10.1007/s10703-016-0257-4.
• [19] Amat N, Dal Zilio S, Hujsa T. Property Directed Reachability for Generalized Petri Nets. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 13243 of LNCS. Springer, 2022 doi:10.1007/978-3-030-99524-9 28.
• [20] Finkel A. The minimal coverability graph for Petri nets. In: International Conference on Application and Theory of Petri Nets (ICATPN). Springer, 1991 doi:10.1007/3-540-56689-9 45.
• [21] Hillah L, Kordon F. Petri Nets Repository: A Tool to Benchmark and Debug Petri Net Tools. In: Application and Theory of Petri Nets and Concurrency (Petri Nets), volume 10258 of LNCS. Springer, 2017 doi:10.1007/978-3-319-57861-3 9.
• [22] de Moura L, Bjørner N. Z3: An Efficient SMT Solver. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 4963 of LNCS. Springer, 2008 doi:10.1007/978-3-540-78800-3 24.
• [23] Bjørner N. The Z3 Theorem Prover. https://github.com/Z3Prover/z3/, 2020.
• [24] Thierry-Mieg Y. Oracle for the MCC 2020 edition. Available at https://github.com/yanntm/pnmcc-models-2020, 2020.
• [25] Thierry-Mieg Y. Structural Reductions Revisited. In: Application and Theory of Petri Nets and Concurrency (Petri Nets), volume 12152 of LNCS. Springer, 2020 doi:10.1007/978-3-030-51831-8 15.
• [26] Lipton RJ. Reduction: a method of proving properties of parallel programs. Communications of the ACM, 1975. 18. doi:10.1145/361227.361234.
• [27] Cohen E, Lamport L. Reduction in TLA. In: Concurrency Theory (CONCUR), volume 1466 of LNCS. Springer, 1998 doi:10.1007/BFb0055631.
• [28] Clarke EM, Grumberg O, Peled D. Model Checking. MIT Press, 1999.
• [29] Schmidt K. Using Petri Net Invariants in State Space Construction. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2619 of LNCS. Springer, 2003 .
• [30] Bønneland FM, Dyhr J, Jensen PG, Johannsen M, Srba J. Stubborn versus structural reductions for Petri nets. Journal of Logical and Algebraic Methods in Programming, 2019. 102. doi:10.1016/j.jlamp.2018.09.002.
• [31] Thierry-Mieg Y. Symbolic and Structural Model-Checking. Fundam. Informaticae, 2021. 183(3-4). doi:10.3233/FI-2021-2090.
• [32] Esparza J, Ledesma-Garza R, Majumdar R, Meyer P, Niksic F. An SMT-Based Approach to Coverability Analysis. In: Computer Aided Verification (CAV), volume 8559 of LNCS. 2014 doi:10.1007/978-3-319-08867-9 40.
• [33] Kang J, Bai Y, Jiao L. Abstraction-Based Incremental Inductive Coverability for Petri Nets. In: Applications and Theory of Petri Nets and Concurrency (Petri Nets), volume 12734 of LNCS. Springer, 2021 doi:10.1007/978-3-030-76983-3 19.
• [34] Kloos J, Majumdar R, Niksic F, Piskac R. Incremental, Inductive Coverability. In: Computer Aided Verification (CAV), volume 8044 of LNCS. Springer, 2013 doi:10.1007/978-3-642-39799-8 10.
• [35] Kosaraju SR. Decidability of Reachability in Vector Addition Systems (Preliminary Version). In: Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing, STOC. ACM, 1982 doi:10.1145/800070.802201.
• [36] Leroux J. The general vector addition system reachability problem by Presburger inductive invariants. In: Logic in Computer Science (LICS). IEEE, 2009 doi:10.1109/LICS.2009.10.
• [37] Dixon A, Lazi´c R. KReach: A Tool for Reachability in Petri Nets. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 12078 of LNCS. Springer, 2020 doi:10.1007/978-3-030-45190-5 22.
• [38] Blondin M, Haase C, Offtermatt P. Directed Reachability for Infinite-State Systems. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 12652 of LNCS. Springer, 2021 doi:10.1007/978-3-030-72013-1 1.
• [39] Conchon S, Goel A, Krstic S, Mebsout A, Za¨ıdi F. Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems. In: Computer Aided Verification (CAV), volume 7358 of LNCS. Springer, 2012 doi:10.1007/978-3-642-31424-7 55.
• [40] Gurfinkel A, Shoham S, Meshman Y. SMT-based verification of parameterized systems. In: International Symposium on Foundations of Software Engineering. ACM, 2016 doi:10.1145/2950290.2950330.
• [41] Amat N, Dal Zilio S, Le Botlan D. Accelerating the Computation of Dead and Concurrent Places Using Reductions. In: Model Checking Software (SPIN), volume 12864 of LNCS. Springer, 2021 doi:10.1007/978-3-030-84629-9 3.