Document

# Regular Model Checking Upside-Down: An Invariant-Based Approach

## File

LIPIcs.CONCUR.2022.23.pdf
• Filesize: 0.86 MB
• 19 pages

## Cite As

Javier Esparza, Mikhail Raskin, and Christoph Welzel. Regular Model Checking Upside-Down: An Invariant-Based Approach. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 23:1-23:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CONCUR.2022.23

## Abstract

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.

## Subject Classification

##### ACM Subject Classification
• Theory of computation → Problems, reductions and completeness
• Theory of computation → Program analysis
• Theory of computation → Invariants
##### Keywords
• parameterized verification
• structural analysis
• regular languages
• regular model-checking
• traps

## Metrics

• Access Statistics
• Total Accesses (updated on a weekly basis)
0

## References

1. Parosh Aziz Abdulla. Regular model checking. Int. J. Softw. Tools Technol. Transf., 14(2):109-118, 2012.
2. 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.
3. 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.
4. 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.
5. 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.
6. Parosh Aziz Abdulla, A. Prasad Sistla, and Muralidhar Talupur. Model checking parameterized systems. In Handbook of Model Checking, pages 685-725. Springer, 2018.
7. 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.
8. 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.
9. 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.
10. 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.
11. Ahmed Bouajjani and Tayssir Touili. Widening techniques for regular tree model checking. Int. J. Softw. Tools Technol. Transf., 14(2):145-165, 2012.
12. 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.
13. Marius Bozga, Radu Iosif, and Joseph Sifakis. Checking deadlock-freedom of parametric component-based systems. J. Log. Algebraic Methods Program., 119:100621, 2021.
14. 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.
15. Dennis Dams, Yassine Lakhnech, and Martin Steffen. Iterating transducers. In CAV, volume 2102 of Lecture Notes in Computer Science, pages 286-297. Springer, 2001.
16. Giorgio Delzanno. Constraint-based verification of parameterized cache coherence protocols. Formal Methods Syst. Des., 23(3):257-301, 2003.
17. 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.
18. Javier Esparza, Mikhail Raskin, and Christoph Welzel. Repository of examples. https://doi.org/10.5281/zenodo.6483615, April 2022.
19. 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.
20. 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.
21. 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.
22. 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.
23. Axel Legay. Extrapolating (omega-)regular model checking. Int. J. Softw. Tools Technol. Transf., 14(2):119-143, 2012.
24. 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.
25. 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.
26. 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.
X

Feedback for Dagstuhl Publishing