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

Authors Javier Esparza , Mikhail Raskin , Christoph Welzel



PDF
Thumbnail PDF

File

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

Document Identifiers

Author Details

Javier Esparza
  • Department of Informatics - I7, Technische Universität München, Germany
Mikhail Raskin
  • Department of Informatics - I7, Technische Universität München, Germany
Christoph Welzel
  • Department of Informatics - I7, Technische Universität München, Germany

Cite AsGet BibTex

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
    PDF Downloads

References

  1. Parosh Aziz Abdulla. Regular model checking. Int. J. Softw. Tools Technol. Transf., 14(2):109-118, 2012. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  6. Parosh Aziz Abdulla, A. Prasad Sistla, and Muralidhar Talupur. Model checking parameterized systems. In Handbook of Model Checking, pages 685-725. Springer, 2018. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  11. Ahmed Bouajjani and Tayssir Touili. Widening techniques for regular tree model checking. Int. J. Softw. Tools Technol. Transf., 14(2):145-165, 2012. Google Scholar
  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. Google Scholar
  13. Marius Bozga, Radu Iosif, and Joseph Sifakis. Checking deadlock-freedom of parametric component-based systems. J. Log. Algebraic Methods Program., 119:100621, 2021. Google Scholar
  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. Google Scholar
  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. Google Scholar
  16. Giorgio Delzanno. Constraint-based verification of parameterized cache coherence protocols. Formal Methods Syst. Des., 23(3):257-301, 2003. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
  23. Axel Legay. Extrapolating (omega-)regular model checking. Int. J. Softw. Tools Technol. Transf., 14(2):119-143, 2012. Google Scholar
  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. Google Scholar
  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. Google Scholar
  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. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail