Document Open Access Logo

Abstract Framework for All-Path Reachability Analysis toward Safety and Liveness Verification

Authors Misaki Kojima , Naoki Nishida

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2026.19.pdf
  • Filesize: 0.89 MB
  • 23 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Rewrite systems
Keywords
  • abstract reduction system
  • reachability
  • cyclic proof
  • runtime-error verification

Metrics

Abstract

An all-path reachability (APR, for short) predicate over an object set is a pair of a source set and a target set, which are subsets of the object set. APR predicates have been defined for abstract reduction systems (ARSs, for short) and then extended to logically constrained term rewrite systems (LCTRSs, for short) as pairs of constrained terms that represent sets of terms modeling configurations, states, etc. An APR predicate is partially (or demonically) valid w.r.t. a rewrite system if every finite maximal reduction sequence of the system starting from any element in the source set includes an element in the target set. Partial validity of APR predicates w.r.t. ARSs is defined by means of two inference rules, which can be considered a proof system to construct (possibly infinite) derivation trees for partial validity. On the other hand, a proof system for LCTRSs consists of four inference rules, leaving a gap between the inference rules for ARSs and LCTRSs. In this paper, we revisit the framework for APR analysis and adapt it to verification of not only safety but also liveness properties. To this end, we first reformulate an abstract framework for partial validity w.r.t. ARSs so that there is a one-to-one correspondence between the inference rules for partial validity w.r.t. ARSs and LCTRSs. Secondly, we show how to apply APR analysis to safety verification. Thirdly, to apply APR analysis to liveness verification, we introduce a novel stronger validity of APR predicates, called total validity, which requires not only finite but also infinite execution paths to reach target sets. Finally, for a partially valid APR predicate with a cyclic-proof tree, we show that the acyclicity of the proof graph obtained from the cyclic-proof tree is a necessary and sufficient condition for total validity. The condition implies that if there exists a cyclic-proof tree for an APR predicate, the proof graph of which is acyclic, then the APR predicate is totally valid.

Cite As Get BibTex

Misaki Kojima and Naoki Nishida. Abstract Framework for All-Path Reachability Analysis toward Safety and Liveness Verification. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 19:1-19:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.FSCD.2026.19

Author Details

Misaki Kojima
  • Graduate School of Informatics, Nagoya University, Japan
Naoki Nishida
  • Graduate School of Informatics, Nagoya University, Japan

Funding

This research was supported by JSPS KAKENHI Grant Number JP24K02900.
  • Kojima, Misaki: Grant-in-Aid for JSPS Fellows Grant Number JP24KJ1240

Acknowledgements

We thank the anonymous reviewers for their valuable feedback, which improved the paper.

References

  1. Franz Baader and Tobias Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. URL: https://doi.org/10.1145/505863.505888.
  2. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  3. James Brotherston. Cyclic proofs for first-order logic with inductive definitions. In Bernhard Beckert, editor, Proceedings of the 14th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, volume 3702 of Lecture Notes in Computer Science, pages 78-92. Springer, 2005. URL: https://doi.org/10.1007/11554554_8.
  4. James Brotherston. Sequent Calculus Proof Systems for Inductive Definitions. PhD thesis, University of Edinburgh, November 2006. Google Scholar
  5. Ştefan Ciobâcă and Dorel Lucanu. A coinductive approach to proving reachability properties in logically constrained term rewriting systems. CoRR, abs/1804.08308, 2018. URL: https://doi.org/10.48550/arXiv.1804.08308.
  6. Ştefan Ciobâcă, Dorel Lucanu, and Andrei-Sebastian Buruiană. Operationally-based program equivalence proofs using LCTRSs. Journal of Logical and Algebraic Methods in Programming, 135:1-22, 2023. URL: https://doi.org/10.1016/j.jlamp.2023.100894.
  7. Ştefan Ciobâcă and Dorel Lucanu. A coinductive approach to proving reachability properties in logically constrained term rewriting systems. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, Proceedings of the 9th International Joint Conference on Automated Reasoning, volume 10900 of Lecture Notes in Computer Science, pages 295-311. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-94205-6_20.
  8. Andrei Ştefănescu, Ştefan Ciobâcă, Radu Mereuta, Brandon M. Moore, Traian-Florin Şerbănuţă, and Grigore Roşu. All-path reachability logic. In Gilles Dowek, editor, Proceedings of the Joint International Conference on Rewriting and Typed Lambda Calculi, volume 8560 of Lecture Notes in Computer Science, pages 425-440. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08918-8_29.
  9. Andrei Ştefănescu, Ştefan Ciobâcă, Radu Mereuta, Brandon M. Moore, Traian-Florin Şerbănuţă, and Grigore Roşu. All-path reachability logic. Logical Methods in Computer Science, 15(2), 2019. URL: https://doi.org/10.23638/LMCS-15(2:5)2019.
  10. Carsten Fuhs, Cynthia Kop, and Naoki Nishida. Verifying procedural programs via constrained rewriting induction. ACM Transactions on Computational Logic, 18(2):14:1-14:50, 2017. URL: https://doi.org/10.1145/3060143.
  11. Yoshiaki Kanazawa and Naoki Nishida. On transforming functions accessing global variables into logically constrained term rewriting systems. In Joachim Niehren and David Sabel, editors, Proceedings of the 5th International Workshop on Rewriting Techniques for Program Transformations and Evaluation, volume 289 of Electronic Proceedings in Theoretical Computer Science, pages 34-52. Open Publishing Association, 2019. URL: https://doi.org/10.4204/EPTCS.289.3.
  12. Yoshiaki Kanazawa, Naoki Nishida, and Masahiko Sakai. On representation of structures and unions in logically constrained rewriting. IEICE Technical Report SS2018-38, the Institute of Electronics, Information and Communication Engineers, 2019. Vol. 118, No. 385, pp. 67-72, in Japanese. Google Scholar
  13. Misaki Kojima. Runtime-Error Verification by Reduction to All-Path Reachability Problems of Constrained Rewriting. PhD thesis, Graduate School of Informatics, Nagoya University, 2024. URL: https://nagoya.repo.nii.ac.jp/records/2010041.
  14. Misaki Kojima and Naoki Nishida. From starvation freedom to all-path reachability problems in constrained rewriting. In Michael Hanus and Daniela Inclezan, editors, Proceedings of the 25th International Symposium on Practical Aspects of Declarative Languages, volume 13880 of Lecture Notes in Computer Science, pages 161-179. Springer Nature Switzerland, 2023. URL: https://doi.org/10.1007/978-3-031-24841-2_11.
  15. Misaki Kojima and Naoki Nishida. Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting. Journal of Logical and Algebraic Methods in Programming, 135:1-19, 2023. URL: https://doi.org/10.1016/j.jlamp.2023.100903.
  16. Misaki Kojima and Naoki Nishida. On solving all-path reachability problems for starvation freedom of concurrent rewrite systems under process fairness. In Laura Kovács and Ana Sokolova, editors, Proceedings of the 18th International Conference on Reachability Problems, volume 15050 of Lecture Notes in Computer Science, pages 54-70. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-72621-7_5.
  17. Misaki Kojima and Naoki Nishida. A sufficient condition of logically constrained term rewrite systems for decidability of all-path reachability problems with constant destinations. Journal of Information Processing, 32:417-435, 2024. URL: https://doi.org/10.2197/IPSJJIP.32.417.
  18. Misaki Kojima and Naoki Nishida. Abstract Framework for All-Path Reachability Analysis toward Safety and Liveness Verification (Full Version). CoRR, abs/2602.04641, 2026. URL: https://doi.org/10.48550/arXiv.2602.04641.
  19. Misaki Kojima, Naoki Nishida, and Yutaka Matsubara. Transforming concurrent programs with semaphores into logically constrained term rewrite systems. Journal of Logical and Algebraic Methods in Programming, 143:1-23, 2025. URL: https://doi.org/10.1016/j.jlamp.2024.101033.
  20. Cynthia Kop and Naoki Nishida. Term rewriting with logical constraints. In Pascal Fontaine, Christophe Ringeissen, and Renate A. Schmidt, editors, Proceedings of the 9th International Symposium on Frontiers of Combining Systems, volume 8152 of Lecture Notes in Computer Science, pages 343-358. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40885-4_24.
  21. Ayuka Matsumi, Naoki Nishida, Misaki Kojima, and Donghoon Shin. On singleton self-loop removal for termination of LCTRSs with bit-vector arithmetic. In Akihisa Yamada, editor, Proceedings of the 19th International Workshop on Termination, pages 1-6, August 2023. URL: https://doi.org/10.48550/arXiv.2307.14094.
  22. Dragana Milovančević, Carsten Fuhs, and Viktor Kunčak. Proving termination of scala programs by constrained term rewriting. In Cynthia Kop and Janis Voigtländer, editors, Informal Proceedings of the 11th International Workshop on Rewriting Techniques for Program Transformations and Evaluation, pages 13-25, July 2025. URL: https://wpte2025.github.io/pre-proceedings.pdf#page=15.
  23. Naoki Nishida and Sarah Winkler. Loop detection by logically constrained term rewriting. In Ruzica Piskac and Philipp Rümmer, editors, Proceedings of the 10th Working Conference on Verified Software: Theories, Tools, and Experiments, volume 11294 of Lecture Notes in Computer Science, pages 309-321. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-03592-1_18.
  24. Enno Ohlebusch. Advanced Topics in Term Rewriting. Springer, 2002. URL: https://doi.org/10.1007/978-1-4757-3661-8.
  25. Grigore Roşu and Traian-Florin Şerbănuţă. An overview of the K semantic framework. Journal of Logic and Algebraic Programming, 79(6):397-434, 2010. URL: https://doi.org/10.1016/j.jlap.2010.03.012.
  26. Sarah Winkler and Aart Middeldorp. Completion for logically constrained rewriting. In Hélène Kirchner, editor, Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, volume 108 of Leibniz International Proceedings in Informatics, pages 30:1-30:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.FSCD.2018.30.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact