Regular Model Checking Upside-Down: An Invariant-Based Approach
Regular model checking is a technique for the verification of infinite-state systems whose configurations can be represented as finite words over a suitable alphabet. It applies to systems whose set of initial configurations is regular, and whose transition relation is captured by a length-preserving transducer. To verify safety properties, regular model checking iteratively computes automata recognizing increasingly larger regular sets of reachable configurations, and checks if they contain unsafe configurations. Since this procedure often does not terminate, acceleration, abstraction, and widening techniques have been developed to compute a regular superset of the reachable configurations.
In this paper we develop a complementary procedure. Instead of approaching the set of reachable configurations from below, we start with the set of all configurations and approach it from above. We use that the set of reachable configurations is equal to the intersection of all inductive invariants of the system. Since this intersection is non-regular in general, we introduce b-bounded invariants, defined as those representable by CNF-formulas with at most b clauses. We prove that, for every b ≥ 0, the intersection of all b-bounded inductive invariants is regular, and we construct an automaton recognizing it. We show that whether this automaton accepts some unsafe configuration is in EXPSPACE for every b ≥ 0, and PSPACE-complete for b = 1. Finally, we study how large must b be to prove safety properties of a number of benchmarks.
parameterized verification
structural analysis
regular languages
regular model-checking
traps
Theory of computation~Problems, reductions and completeness
Theory of computation~Program analysis
Theory of computation~Invariants
23:1-23:19
Regular Paper
The project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme under grant agreement No 787367 (PaVeS).
https://doi.org/10.5281/zenodo.6483615
https://arxiv.org/abs/2205.03060
Javier
Esparza
Javier Esparza
Department of Informatics - I7, Technische Universität München, Germany
https://orcid.org/0000-0001-9862-4919
Mikhail
Raskin
Mikhail Raskin
Department of Informatics - I7, Technische Universität München, Germany
https://orcid.org/0000-0002-6660-5673
Christoph
Welzel
Christoph Welzel
Department of Informatics - I7, Technische Universität München, Germany
https://orcid.org/0000-0001-5583-0640
10.4230/LIPIcs.CONCUR.2022.23
Parosh Aziz Abdulla. Regular model checking. Int. J. Softw. Tools Technol. Transf., 14(2):109-118, 2012.
Parosh Aziz Abdulla. Regular model checking: Evolution and perspectives. In Model Checking, Synthesis, and Learning, volume 13030 of Lecture Notes in Computer Science, pages 78-96. Springer, 2021.
Parosh Aziz Abdulla, Giorgio Delzanno, Noomene Ben Henda, and Ahmed Rezine. Regular model checking without transducers (on efficient verification of parameterized systems). In TACAS, volume 4424 of Lecture Notes in Computer Science, pages 721-736. Springer, 2007.
Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, and Julien d'Orso. Regular model checking made simple and efficient. In CONCUR, volume 2421 of Lecture Notes in Computer Science, pages 116-130. Springer, 2002.
Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, and Mayank Saksena. A survey of regular model checking. In CONCUR, volume 3170 of Lecture Notes in Computer Science, pages 35-48. Springer, 2004.
Parosh Aziz Abdulla, A. Prasad Sistla, and Muralidhar Talupur. Model checking parameterized systems. In Handbook of Model Checking, pages 685-725. Springer, 2018.
Bernard Boigelot, Axel Legay, and Pierre Wolper. Iterating transducers in the large (extended abstract). In CAV, volume 2725 of Lecture Notes in Computer Science, pages 223-235. Springer, 2003.
Ahmed Bouajjani, Peter Habermehl, Adam Rogalewicz, and Tomás Vojnar. Abstract regular (tree) model checking. Int. J. Softw. Tools Technol. Transf., 14(2):167-191, 2012.
Ahmed Bouajjani, Peter Habermehl, and Tomás Vojnar. Abstract regular model checking. In CAV, volume 3114 of Lecture Notes in Computer Science, pages 372-386. Springer, 2004.
Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson, and Tayssir Touili. Regular model checking. In CAV, volume 1855 of Lecture Notes in Computer Science, pages 403-418. Springer, 2000.
Ahmed Bouajjani and Tayssir Touili. Widening techniques for regular tree model checking. Int. J. Softw. Tools Technol. Transf., 14(2):145-165, 2012.
Marius Bozga, Javier Esparza, Radu Iosif, Joseph Sifakis, and Christoph Welzel. Structural invariants for the verification of systems with parameterized architectures. In TACAS (1), volume 12078 of Lecture Notes in Computer Science, pages 228-246. Springer, 2020.
Marius Bozga, Radu Iosif, and Joseph Sifakis. Checking deadlock-freedom of parametric component-based systems. J. Log. Algebraic Methods Program., 119:100621, 2021.
Yu-Fang Chen, Chih-Duo Hong, Anthony W. Lin, and Philipp Rümmer. Learning to prove safety over parameterised concurrent systems. In FMCAD, pages 76-83. IEEE, 2017.
Dennis Dams, Yassine Lakhnech, and Martin Steffen. Iterating transducers. In CAV, volume 2102 of Lecture Notes in Computer Science, pages 286-297. Springer, 2001.
Giorgio Delzanno. Constraint-based verification of parameterized cache coherence protocols. Formal Methods Syst. Des., 23(3):257-301, 2003.
Jacob Elgaard, Nils Klarlund, and Anders Møller. MONA 1.x: new techniques for WS1S and WS2S. In Proc. 10th International Conference on Computer-Aided Verification, CAV '98, volume 1427 of LNCS, pages 516-520. Springer-Verlag, June/July 1998.
Javier Esparza, Mikhail Raskin, and Christoph Welzel. Repository of examples. https://doi.org/10.5281/zenodo.6483615, April 2022.
https://doi.org/10.5281/zenodo.6483615
Javier Esparza, Mikhail A. Raskin, and Christoph Welzel. Abduction of trap invariants in parameterized systems. In GandALF, volume 346 of EPTCS, pages 1-17, 2021.
Javier Esparza, Mikhail A. Raskin, and Christoph Welzel. Computing parameterized invariants of parameterized petri nets. In Petri Nets, volume 12734 of Lecture Notes in Computer Science, pages 141-163. Springer, 2021.
Javier Esparza, Mikhail A. Raskin, and Christoph Welzel. Regular model checking upside-down: An invariant-based approach. CoRR, abs/2205.03060, 2022. URL: http://arxiv.org/abs/2205.03060.
http://arxiv.org/abs/2205.03060
Bengt Jonsson and Marcus Nilsson. Transitive closures of regular relations for verifying infinite-state systems. In TACAS, volume 1785 of Lecture Notes in Computer Science, pages 220-234. Springer, 2000.
Axel Legay. Extrapolating (omega-)regular model checking. Int. J. Softw. Tools Technol. Transf., 14(2):119-143, 2012.
Kenneth L. McMillan and Oded Padon. Ivy: A multi-modal verification tool for distributed algorithms. In CAV (2), volume 12225 of Lecture Notes in Computer Science, pages 190-202. Springer, 2020.
Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, and Sharon Shoham. Ivy: safety verification by interactive generalization. In PLDI, pages 614-630. ACM, 2016.
Amir Pnueli, Sitvanit Ruah, and Lenore D. Zuck. Automatic deductive verification with invisible invariants. In TACAS, volume 2031 of Lecture Notes in Computer Science, pages 82-97. Springer, 2001.
Javier Esparza, Mikhail Raskin, and Christoph Welzel
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode