Document Open Access Logo

Computing Inductive Invariants of Regular Abstraction Frameworks

Authors Philipp Czerner , Javier Esparza , Valentin Krasotin , Christoph Welzel-Mohr

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2024.19.pdf
  • Filesize: 0.89 MB
  • 18 pages

Document Identifiers

Author Details

Philipp Czerner
  • Technical University of Munich, Germany
Javier Esparza
  • Technical University of Munich, Germany
Valentin Krasotin
  • Technical University of Munich, Germany
Christoph Welzel-Mohr
  • Technical University of Munich, Germany

Cite AsGet BibTex

Philipp Czerner, Javier Esparza, Valentin Krasotin, and Christoph Welzel-Mohr. Computing Inductive Invariants of Regular Abstraction Frameworks. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CONCUR.2024.19

Abstract

Regular transition systems (RTS) are a popular formalism for modeling infinite-state systems in general, and parameterised systems in particular. In a CONCUR 22 paper, Esparza et al. introduce a novel approach to the verification of RTS, based on inductive invariants. The approach computes the intersection of all inductive invariants of a given RTS that can be expressed as CNF formulas with a bounded number of clauses, and uses it to construct an automaton recognising an overapproximation of the reachable configurations. The paper shows that the problem of deciding if the language of this automaton intersects a given regular set of unsafe configurations is in EXPSPACE and PSPACE-hard. We introduce regular abstraction frameworks, a generalisation of the approach of Esparza et al., very similar to the regular abstractions of Hong and Lin. A framework consists of a regular language of constraints, and a transducer, called the interpretation, that assigns to each constraint the set of configurations of the RTS satisfying it. Examples of regular abstraction frameworks include the formulas of Esparza et al., octagons, bounded difference matrices, and views. We show that the generalisation of the decision problem above to regular abstraction frameworks remains in EXPSPACE, and prove a matching (non-trivial) EXPSPACE-hardness bound. EXPSPACE-hardness implies that, in the worst case, the automaton recognising the overapproximation of the reachable configurations has a double-exponential number of states. We introduce a learning algorithm that computes this automaton in a lazy manner, stopping whenever the current hypothesis is already strong enough to prove safety. We report on an implementation and show that our experimental results improve on those of Esparza et al.

Subject Classification

ACM Subject Classification
  • Theory of computation → Regular languages
  • Theory of computation → Problems, reductions and completeness
  • Theory of computation → Verification by model checking
Keywords
  • Regular model checking
  • abstraction
  • inductive invariants

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

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, Frédéric Haziza, and Lukás Holík. Parameterized verification through view abstraction. Int. J. Softw. Tools Technol. Transf., 18(5):495-516, 2016. 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. Dana Angluin. Learning regular sets from queries and counterexamples. Inf. Comput., 75(2):87-106, 1987. Google Scholar
  8. Clark W. Barrett and Cesare Tinelli. Satisfiability modulo theories. In Handbook of Model Checking, pages 305-343. Springer, 2018. Google Scholar
  9. Daniel Le Berre and Anne Parrain. The sat4j library, release 2.2. J. Satisf. Boolean Model. Comput., 7(2-3):59-6, 2010. Google Scholar
  10. 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
  11. 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
  12. 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
  13. 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
  14. 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
  15. 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
  16. Philipp Czerner, Javier Esparza, Valentin Krasotin, and Christoph Welzel-Mohr. Computing inductive invariants of regular abstraction frameworks. CoRR, abs/2404.10752, 2024. URL: https://doi.org/10.48550/arXiv.2404.10752.
  17. 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
  18. Javier Esparza and Michael Blondin. Automata Theory - An Algorithmic Approach. MIT Press, 2023. Google Scholar
  19. Javier Esparza, Mikhail A. Raskin, and Christoph Welzel. Regular model checking upside-down: An invariant-based approach. In CONCUR, volume 243 of LIPIcs, pages 23:1-23:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. Google Scholar
  20. Javier Esparza, Mikhail A. Raskin, and Christoph Welzel. Regular model checking upside-down: An invariant-based approach. CoRR, abs/2205.03060, version 2, 2022. Google Scholar
  21. Chih-Duo Hong and Anthony W. Lin. Regular abstractions for array systems. Proc. ACM Program. Lang., 8(POPL):638-666, 2024. Google Scholar
  22. Malte Isberner, Falk Howar, and Bernhard Steffen. The open-source learnlib - A framework for active automata learning. In CAV (1), volume 9206 of Lecture Notes in Computer Science, pages 487-495. Springer, 2015. Google Scholar
  23. 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
  24. Yonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, and Elad Shahar. Symbolic model checking with rich assertional languages. Theor. Comput. Sci., 256(1-2):93-112, 2001. Google Scholar
  25. Daniel Kroening and Ofer Strichman. Decision Procedures - An Algorithmic Point of View, Second Edition. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2016. Google Scholar
  26. Axel Legay. Extrapolating (omega-)regular model checking. Int. J. Softw. Tools Technol. Transf., 14(2):119-143, 2012. Google Scholar
  27. Antoine Miné. The octagon abstract domain. High. Order Symb. Comput., 19(1):31-100, 2006. Google Scholar
  28. Daniel Neider. Applications of automata learning in verification and synthesis. PhD thesis, RWTH Aachen University, 2014. Google Scholar
  29. Daniel Neider and Nils Jansen. Regular model checking using solver technologies and automata learning. In NASA Formal Methods, volume 7871 of Lecture Notes in Computer Science, pages 16-31. Springer, 2013. Google Scholar
  30. Bernhard Steffen, Falk Howar, and Maik Merten. Introduction to active automata learning from a practical perspective. In SFM, volume 6659 of Lecture Notes in Computer Science, pages 256-296. Springer, 2011. Google Scholar
  31. Abhay Vardhan. Learning To Verify Systems. PhD thesis, University of Illinois, 2006. Google Scholar
  32. Abhay Vardhan, Koushik Sen, Mahesh Viswanathan, and Gul Agha. Learning to verify safety properties. In ICFEM, volume 3308 of Lecture Notes in Computer Science, pages 274-289. Springer, 2004. Google Scholar
  33. Christoph Welzel-Mohr, Valentin Krasotin, Philipp Czerner, and Javier Esparza. dodo, February 2024. URL: https://doi.org/10.5281/zenodo.12734991.
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact