Document Open Access Logo

Regular Model Checking for Systems with Effectively Regular Reachability Relation

Authors Javier Esparza , Valentin Krasotin

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2025.45.pdf
  • Filesize: 0.79 MB
  • 19 pages

Document Identifiers

Related Versions

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

Abstract

Regular model checking is a well-established technique for the verification of regular transition systems (RTS): transition systems whose initial configurations and transition relation can be effectively encoded as regular languages. In 2008, To and Libkin studied RTSs in which the reachability relation (the reflexive and transitive closure of the transition relation) is also effectively regular, and showed that the recurrent reachability problem (whether a regular set L of configurations is reached infinitely often) is polynomial in the size of RTS and the transducer for the reachability relation. We extend the work of To and Libkin by studying the decidability and complexity of verifying almost-sure reachability and recurrent reachability - that is, whether L is reachable or recurrently reachable with probability 1. We then apply our results to the more common case in which only a regular overapproximation of the reachability relation is available. In particular, we extend recent complexity results on verifying safety using regular abstraction frameworks - a technique recently introduced by Czerner, the authors, and Welzel-Mohr - to liveness and almost-sure properties.

Cite As Get BibTex

Javier Esparza and Valentin Krasotin. Regular Model Checking for Systems with Effectively Regular Reachability Relation. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 45:1-45:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.MFCS.2025.45

Author Details

Javier Esparza
  • Technical University of Munich, Germany
Valentin Krasotin
  • Technical University of Munich, Germany

Acknowledgements

We thank Anthony Widjaja Lin and Pascal Bergsträßer for very insightful discussions, and the anonymous reviewers for helpful comments.

References

  1. Parosh Aziz Abdulla. Regular model checking. Int. J. Softw. Tools Technol. Transf., 14(2):109-118, 2012. URL: https://doi.org/10.1007/S10009-011-0216-8.
  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. URL: https://doi.org/10.1007/978-3-030-91384-7_5.
  3. Parosh Aziz Abdulla, Christel Baier, S. Purushothaman Iyer, and Bengt Jonsson. Reasoning about probabilistic lossy channel systems. In CONCUR, volume 1877 of Lecture Notes in Computer Science, pages 320-333. Springer, 2000. URL: https://doi.org/10.1007/3-540-44618-4_24.
  4. Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Yih-Kuen Tsay. General decidability theorems for infinite-state systems. In LICS, pages 313-321. IEEE Computer Society, 1996. URL: https://doi.org/10.1109/LICS.1996.561359.
  5. Parosh Aziz Abdulla, Aurore Collomb-Annichini, Ahmed Bouajjani, and Bengt Jonsson. Using forward reachability analysis for verification of lossy channel systems. Formal Methods Syst. Des., 25(1):39-65, 2004. URL: https://doi.org/10.1023/B:FORM.0000033962.51898.1A.
  6. 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. URL: https://doi.org/10.1007/S10009-015-0406-X.
  7. Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. In LICS, pages 160-170. IEEE Computer Society, 1993. URL: https://doi.org/10.1109/LICS.1993.287591.
  8. 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. URL: https://doi.org/10.1007/3-540-45694-5_9.
  9. 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. URL: https://doi.org/10.1007/978-3-540-28644-8_3.
  10. Parosh Aziz Abdulla, A. Prasad Sistla, and Muralidhar Talupur. Model checking parameterized systems. In Handbook of Model Checking, pages 685-725. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-10575-8_21.
  11. Dana Angluin, James Aspnes, Zoë Diamadi, Michael J. Fischer, and René Peralta. Computation in networks of passively mobile finite-state sensors. Distributed Comput., 18(4):235-253, 2006. URL: https://doi.org/10.1007/S00446-005-0138-3.
  12. Pascal Bergsträßer, Moses Ganardi, Anthony W. Lin, and Georg Zetzsche. Ramsey quantifiers over automatic structures: Complexity and applications to verification. In Christel Baier and Dana Fisman, editors, LICS, pages 28:1-28:14. ACM, 2022. URL: https://doi.org/10.1145/3531130.3533346.
  13. Michael Blondin and Mikhail A. Raskin. The complexity of reachability in affine vector addition systems with states. Log. Methods Comput. Sci., 17(3), 2021. URL: https://doi.org/10.46298/LMCS-17(3:3)2021.
  14. 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. URL: https://doi.org/10.1007/10722167_31.
  15. Laura Bozzelli and Pierre Ganty. Complexity analysis of the backward coverability algorithm for VASS. In RP, volume 6945 of Lecture Notes in Computer Science, pages 96-109. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-24288-5_10.
  16. Søren Christensen, Yoram Hirshfeld, and Faron Moller. Bisimulation equivalence is decidable for basic parallel processes. In CONCUR, volume 715 of Lecture Notes in Computer Science, pages 143-157. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_11.
  17. Søren Christensen, Yoram Hirshfeld, and Faron Moller. Decomposability, decidability and axiomatisability for bisimulation equivalence on basic parallel processes. In LICS, pages 386-396. IEEE Computer Society, 1993. URL: https://doi.org/10.1109/LICS.1993.287569.
  18. Patrick Cousot. Principles of abstract interpretation. MIT Press, 2021. Google Scholar
  19. Philipp Czerner, Javier Esparza, Valentin Krasotin, and Christoph Welzel-Mohr. Computing inductive invariants of regular abstraction frameworks. In CONCUR, volume 311 of LIPIcs, pages 19:1-19:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPICS.CONCUR.2024.19.
  20. Wojciech Czerwinski, Slawomir Lasota, Ranko Lazic, Jérôme Leroux, and Filip Mazowiecki. The reachability problem for petri nets is not elementary. J. ACM, 68(1):7:1-7:28, 2021. URL: https://doi.org/10.1145/3422822.
  21. Wojciech Czerwinski and Lukasz Orlikowski. Reachability in vector addition systems is ackermann-complete. In FOCS, pages 1229-1240. IEEE, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00120.
  22. E. Allen Emerson and Kedar S. Namjoshi. Automatic verification of parameterized synchronous systems (extended abstract). In CAV, volume 1102 of Lecture Notes in Computer Science, pages 87-98. Springer, 1996. URL: https://doi.org/10.1007/3-540-61474-5_60.
  23. Javier Esparza. Petri nets, commutative context-free grammars, and basic parallel processes. In FCT, volume 965 of Lecture Notes in Computer Science, pages 221-232. Springer, 1995. URL: https://doi.org/10.1007/3-540-60249-6_54.
  24. Javier Esparza. Decidability of model checking for infinite-state concurrent systems. Acta Informatica, 34(2):85-107, 1997. URL: https://doi.org/10.1007/S002360050074.
  25. Javier Esparza and Michael Blondin. Automata Theory - An Algorithmic Approach. MIT Press, 2023. Google Scholar
  26. Javier Esparza and Michael Blondin. Automata theory: An algorithmic approach. MIT Press, 2023. Google Scholar
  27. Javier Esparza, Alain Finkel, and Richard Mayr. On the verification of broadcast protocols. In LICS, pages 352-359. IEEE Computer Society, 1999. URL: https://doi.org/10.1109/LICS.1999.782630.
  28. Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar. Model checking population protocols. In FSTTCS, volume 65 of LIPIcs, pages 27:1-27:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPICS.FSTTCS.2016.27.
  29. Javier Esparza and Astrid Kiehn. On the model checking problem for branching time logics and basic parallel processes. In CAV, volume 939 of Lecture Notes in Computer Science, pages 353-366. Springer, 1995. URL: https://doi.org/10.1007/3-540-60045-0_62.
  30. Javier Esparza and Valentin Krasotin. Regular model checking for systems with effectively regular reachability relation, 2025. URL: https://arxiv.org/abs/2506.18833.
  31. Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere! Theor. Comput. Sci., 256(1-2):63-92, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00102-X.
  32. Christoph Haase. A survival guide to presburger arithmetic. ACM SIGLOG News, 5(3):67-82, 2018. URL: https://doi.org/10.1145/3242953.3242964.
  33. David Harel, Amir Pnueli, and Jonathan Stavi. Propositional dynamic logic of nonregular programs. J. Comput. Syst. Sci., 26(2):222-243, 1983. URL: https://doi.org/10.1016/0022-0000(83)90014-4.
  34. Graham Higman. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society, 3(1):326-336, 1952. Google Scholar
  35. Chih-Duo Hong and Anthony W. Lin. Regular abstractions for array systems. Proc. ACM Program. Lang., 8(POPL):638-666, 2024. URL: https://doi.org/10.1145/3632864.
  36. John E. Hopcroft and Jean-Jacques Pansiot. On the reachability problem for 5-dimensional vector addition systems. Theor. Comput. Sci., 8:135-159, 1979. URL: https://doi.org/10.1016/0304-3975(79)90041-0.
  37. S. Purushothaman Iyer and Murali Narasimha. Probabilistic lossy channel systems. In TAPSOFT, volume 1214 of Lecture Notes in Computer Science, pages 667-681. Springer, 1997. URL: https://doi.org/10.1007/BFB0030633.
  38. Ondrej Lengál, Anthony Widjaja Lin, Rupak Majumdar, and Philipp Rümmer. Fair termination for parameterized probabilistic concurrent systems. In TACAS (1), volume 10205 of Lecture Notes in Computer Science, pages 499-517, 2017. URL: https://doi.org/10.1007/978-3-662-54577-5_29.
  39. Jérôme Leroux. The reachability problem for petri nets is not primitive recursive. In FOCS, pages 1241-1252. IEEE, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00121.
  40. Anthony W. Lin and Philipp Rümmer. Liveness of randomised parameterised systems under arbitrary schedulers. In CAV (2), volume 9780 of Lecture Notes in Computer Science, pages 112-133. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-41540-6_7.
  41. Tadao Murata. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4):541-580, 1989. URL: https://doi.org/10.1109/5.24143.
  42. Piergiorgio Odifreddi. Classical recursion theory: The theory of functions and sets of natural numbers, volume 125. Elsevier, 1992. Google Scholar
  43. Anthony Widjaja To and Leonid Libkin. Recurrent reachability analysis in regular model checking. In LPAR, volume 5330 of Lecture Notes in Computer Science, pages 198-213. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-89439-1_15.
  44. Anthony Widjaja To and Leonid Libkin. Algorithmic metatheorems for decidable LTL model checking over infinite systems. In FoSSaCS, volume 6014 of Lecture Notes in Computer Science, pages 221-236. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-12032-9_16.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact