Document Open Access Logo

Complete ω-Regular Supermartingale Certificates

Authors Alessandro Abate , Mirco Giacobbe , Sergey Ichtchenko , Diptarko Roy

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.3.pdf
  • Filesize: 1.85 MB
  • 28 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Probabilistic computation
Keywords
  • Probabilistic Model Checking
  • Markov Chains on Measurable State Spaces
  • Omega-Regular Properties
  • Martingale Theory

Metrics

Abstract

We introduce a general methodology for the construction of sound and complete proof rules for the almost-sure and quantitative acceptance of reactivity properties on time-homogeneous Markov chains with general state spaces. Reactivity captures ω-regular properties and subsumes linear temporal logic. Our core technical result establishes that every reactivity property admits decomposition into multiple obligations of almost-sure termination into absorbing regions, and that appropriate absorbing regions always exist on general state spaces. This enables the extension of every complete proof rule for almost-sure termination into a proof rule for reactivity that is complete in the almost-sure case, and complete up to an arbitrarily small ε-approximation in the quantitative case. We apply our new methodology to recent results on sound and complete supermartingale certificates for almost-sure termination in the special case of countably infinite state spaces, alongside standard results on quantitative safety. As a result, we obtain the first sound and complete supermartingale certificates for almost-sure ω-regular properties and the first sound and ε-complete supermartingale certificates for quantitative ω-regular properties on time-homogeneous Markov chains with countably infinite state spaces.

Cite As Get BibTex

Alessandro Abate, Mirco Giacobbe, Sergey Ichtchenko, and Diptarko Roy. Complete ω-Regular Supermartingale Certificates. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 3:1-3:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.3

Author Details

Alessandro Abate
  • University of Oxford, UK
Mirco Giacobbe
  • University of Birmingham, UK
Sergey Ichtchenko
  • University of Oxford, UK
Diptarko Roy
  • University of Birmingham, UK

Funding

This work was supported in part by the Advanced Research and Invention Agency under the Safeguarded AI programme.

References

  1. Alessandro Abate, Alec Edwards, Mirco Giacobbe, Hashan Punchihewa, and Diptarko Roy. Quantitative verification with neural networks. Log. Methods Comput. Sci., 22(2), 2026. URL: https://doi.org/10.46298/LMCS-22(2:4)2026.
  2. Alessandro Abate, Mirco Giacobbe, and Diptarko Roy. Learning probabilistic termination proofs. In CAV (2), volume 12760 of Lecture Notes in Computer Science, pages 3-26. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-81688-9_1.
  3. Alessandro Abate, Mirco Giacobbe, and Diptarko Roy. Stochastic omega-regular verification and control with supermartingales. In CAV (3), volume 14683 of Lecture Notes in Computer Science, pages 395-419. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-65633-0_18.
  4. Alessandro Abate, Mirco Giacobbe, and Diptarko Roy. Quantitative supermartingale certificates. In CAV (2), volume 15932 of Lecture Notes in Computer Science, pages 3-28. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-98679-6_1.
  5. Sheshansh Agrawal, Krishnendu Chatterjee, and Petr Novotný. Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. Proc. ACM Program. Lang., 2(POPL):34:1-34:32, 2018. URL: https://doi.org/10.1145/3158122.
  6. Daniele Ahmed, Andrea Peruffo, and Alessandro Abate. Automated and sound synthesis of lyapunov functions with SMT solvers. In TACAS (1), volume 12078 of Lecture Notes in Computer Science, pages 97-114. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-45190-5_6.
  7. Matin Ansaripour, Krishnendu Chatterjee, Thomas A. Henzinger, Mathias Lechner, and Ðorđe Žikelić. Learning provably stabilizing neural controllers for discrete-time stochastic systems. In ATVA (1), volume 14215 of Lecture Notes in Computer Science, pages 357-379. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-45329-8_17.
  8. Ali Asadi, Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady, and Mohammad Mahdavi. Polynomial reachability witnesses via stellensätze. In PLDI, pages 772-787. ACM, 2021. URL: https://doi.org/10.1145/3453483.3454076.
  9. S. Axler. Measure, Integration & Real Analysis. Graduate Texts in Mathematics. Springer International Publishing, 2019. Google Scholar
  10. Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. Probabilistic program verification via inductive synthesis of inductive invariants. In TACAS (2), volume 13994 of Lecture Notes in Computer Science, pages 410-429. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30820-8_25.
  11. Aleksandar Chakarov and Sriram Sankaranarayanan. Probabilistic program analysis with martingales. In CAV, volume 8044 of Lecture Notes in Computer Science, pages 511-526. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39799-8_34.
  12. Aleksandar Chakarov, Yuen-Lam Voronin, and Sriram Sankaranarayanan. Deductive proofs of almost sure persistence and recurrence properties. In TACAS, volume 9636 of Lecture Notes in Computer Science, pages 260-279. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49674-9_15.
  13. Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. Termination analysis of probabilistic programs through positivstellensatz’s. In CAV (1), volume 9779 of Lecture Notes in Computer Science, pages 3-22. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-41528-4_1.
  14. Krishnendu Chatterjee, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. ACM Trans. Program. Lang. Syst., 40(2):7:1-7:45, 2018. URL: https://doi.org/10.1145/3174800.
  15. Krishnendu Chatterjee, Amir Kafshdar Goharshady, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, and Ðorđe Žikelić. Sound and complete witnesses for template-based verification of LTL properties on polynomial programs. In FM (1), volume 14933 of Lecture Notes in Computer Science, pages 600-619. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-71162-6_31.
  16. Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, and Dorde Zikelic. Sound and complete certificates for quantitative termination analysis of probabilistic programs. In CAV (1), Lecture Notes in Computer Science, pages 55-78. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-13185-1_4.
  17. Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Mehrdad Karrabi, Harshit J. Motwani, Maximilian Seeliger, and Ðorđe Žikelić. Quantified linear and polynomial arithmetic satisfiability via template-based skolemization. In AAAI, pages 7326-7336. AAAI Press, 2025. Google Scholar
  18. Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný, and Ðorđe Žikelić. Equivalence and similarity refutation for probabilistic programs. Proc. ACM Program. Lang., 8(PLDI):2098-2122, 2024. URL: https://doi.org/10.1145/3656462.
  19. Krishnendu Chatterjee, Thomas A. Henzinger, Mathias Lechner, and Ðorđe Žikelić. A learner-verifier framework for neural network controllers and certificates of stochastic systems. In TACAS (1), volume 13993 of Lecture Notes in Computer Science, pages 3-25. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-30823-9_1.
  20. Krishnendu Chatterjee, Petr Novotný, and Ðorđe Žikelić. Stochastic invariants for probabilistic termination. In POPL, pages 145-160. ACM, 2017. URL: https://doi.org/10.1145/3009837.3009873.
  21. Michael Colón, Sriram Sankaranarayanan, and Henny Sipma. Linear invariant generation using non-linear constraint solving. In CAV, volume 2725 of Lecture Notes in Computer Science, pages 420-432. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45069-6_39.
  22. Michael Colón and Henny Sipma. Synthesis of linear ranking functions. In TACAS, volume 2031 of Lecture Notes in Computer Science, pages 67-81. Springer, 2001. URL: https://doi.org/10.1007/3-540-45319-9_6.
  23. Michael Colón and Henny Sipma. Practical methods for proving program termination. In CAV, volume 2404 of Lecture Notes in Computer Science, pages 442-454. Springer, 2002. URL: https://doi.org/10.1007/3-540-45657-0_36.
  24. W. Doblin. éléments d'une théorie générale des chaînes simples constantes de Markoff. Annales scientifiques de l'École Normale Supérieure, 3e série, 57:61-111, 1940. URL: https://doi.org/10.24033/asens.883.
  25. R. Douc, E. Moulines, P. Priouret, and P. Soulier. Markov Chains. Springer Series in Operations Research and Financial Engineering. Springer, 2018. Google Scholar
  26. Rick Durrett. Probability: Theory and Examples, 4th Edition. Cambridge University Press, 2010. URL: https://doi.org/10.1017/CBO9780511779398.
  27. Michael D. Ernst, Jeff H. Perkins, Philip J. Guo, Stephen McCamant, Carlos Pacheco, Matthew S. Tschantz, and Chen Xiao. The daikon system for dynamic detection of likely invariants. Sci. Comput. Program., 69(1-3):35-45, 2007. URL: https://doi.org/10.1016/J.SCICO.2007.01.015.
  28. F. G. Foster. On the Stochastic Matrices Associated with Certain Queuing Processes. The Annals of Mathematical Statistics, 24(3):355-360, 1953. URL: https://doi.org/10.1214/aoms/1177728976.
  29. Mirco Giacobbe, Daniel Kroening, Abhinandan Pal, and Michael Tautschnig. Neural model checking. In NeurIPS, 2024. Google Scholar
  30. Mirco Giacobbe, Daniel Kroening, Abhinandan Pal, and Michael Tautschnig. Let a neural network be your invariant. In NeurIPS, 2025. Google Scholar
  31. David Handelman. Representing polynomials by positive linear functions on compact convex polyhedra. Pacific Journal of Mathematics, 132, March 1988. Google Scholar
  32. Thomas A. Henzinger, Kaushik Mallik, Pouya Sadeghi, and Ðorđe Žikelić. Supermartingale certificates for quantitative omega-regular verification and control. In CAV (2), volume 15932 of Lecture Notes in Computer Science, pages 29-55. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-98679-6_2.
  33. Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Patrick Totzke. Büchi objectives in countable mdps. In ICALP, volume 132 of LIPIcs, pages 119:1-119:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.119.
  34. Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Patrick Totzke. Strategy complexity of parity objectives in countable MDPs. In CONCUR, volume 171 of LIPIcs, pages 39:1-39:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.39.
  35. Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Patrick Totzke. Transience in countable mdps. In CONCUR, volume 203 of LIPIcs, pages 11:1-11:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2021.11.
  36. Stefan Kiefer, Richard Mayr, Mahsa Shirmohammadi, and Patrick Totzke. Strategy complexity of Büchi and transience objectives in concurrent stochastic games. In EC, pages 390-409. ACM, 2025. URL: https://doi.org/10.1145/3736252.3742560.
  37. Satoshi Kura and Hiroshi Unno. A hierarchy of supermartingales for ω-regular verification. CoRR, abs/2512.00270, 2025. URL: https://doi.org/10.48550/arXiv.2512.00270.
  38. H.J. Kushner. Stochastic Stability and Control. Mathematics in science and engineering. Academic Press, 1967. Google Scholar
  39. Mathias Lechner, Ðorđe Žikelić, Krishnendu Chatterjee, and Thomas A. Henzinger. Stability verification in stochastic control systems via neural network supermartingales. In AAAI, pages 7326-7336. AAAI Press, 2022. URL: https://doi.org/10.1609/AAAI.V36I7.20695.
  40. Rupak Majumdar and V. R. Sathiyanarayana. Sound and complete proof rules for probabilistic termination. Proc. ACM Program. Lang., 9(POPL):1871-1902, 2025. URL: https://doi.org/10.1145/3704899.
  41. Zohar Manna and Amir Pnueli. A hierarchy of temporal properties. In PODC, pages 377-410. ACM, 1990. URL: https://doi.org/10.1145/93385.93442.
  42. Zohar Manna and Amir Pnueli. Temporal verification of reactive systems - safety. Springer, 1995. Google Scholar
  43. Annabelle McIver, Carroll Morgan, Benjamin Lucien Kaminski, and Joost-Pieter Katoen. A new proof rule for almost-sure termination. Proc. ACM Program. Lang., 2(POPL):33:1-33:28, 2018. URL: https://doi.org/10.1145/3158121.
  44. Jean-François Mertens, Ester Samuel-Cahn, and Shmuel Zamir. Necessary and sufficient conditions for recurrence and transience of markov chains, in terms of inequalities. Journal of Applied Probability, 15(4):848-851, 1978. URL: http://www.jstor.org/stable/3213440.
  45. Sean Meyn and Richard L. Tweedie. Markov Chains and Stochastic Stability. Cambridge Mathematical Library. Cambridge University Press, 2 edition, 2009. Google Scholar
  46. Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, and Laura Kovács. The probabilistic termination tool amber. In Marieke Huisman, Corina Păsăreanu, and Naijun Zhan, editors, Formal Methods, pages 667-675, Cham, 2021. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-90870-6_36.
  47. Marcel Moosbrugger, Miroslav Stankovic, Ezio Bartocci, and Laura Kovács. This is the moment for probabilistic loops. Proc. ACM Program. Lang., 6(OOPSLA2):1497-1525, 2022. URL: https://doi.org/10.1145/3563341.
  48. Grigory Neustroev, Mirco Giacobbe, and Anna Lukina. Neural continuous-time supermartingale certificates. In AAAI. AAAI Press, 2025. URL: https://doi.org/10.1609/AAAI.V39I26.34966.
  49. ThanhVu Nguyen, Deepak Kapur, Westley Weimer, and Stephanie Forrest. DIG: A dynamic invariant generator for polynomial and array invariants. ACM Trans. Softw. Eng. Methodol., 23(4):30:1-30:30, 2014. URL: https://doi.org/10.1145/2556782.
  50. A. G. Pakes. Some conditions for ergodicity and recurrence of markov chains. Operations Research, 17(6):1058-1061, 1969. URL: https://doi.org/10.1287/OPRE.17.6.1058.
  51. Antonis Papachristodoulou and Stephen Prajna. On the construction of lyapunov functions using the sum of squares decomposition. In CDC, pages 3482-3487. IEEE, 2002. URL: https://doi.org/10.1109/CDC.2002.1184414.
  52. David Pollard. A User’s Guide to Measure Theoretic Probability. Cambridge Series in Statistical and Probabilistic Mathematics. Cambridge University Press, 2001. Google Scholar
  53. Stephen Prajna, Ali Jadbabaie, and George J. Pappas. Stochastic safety verification using barrier certificates. In CDC, pages 929-934. IEEE, 2004. URL: https://doi.org/10.1109/CDC.2004.1428804.
  54. Stephen Prajna, Antonis Papachristodoulou, and Pablo A. Parrilo. Introducing SOSTOOLS: a general purpose sum of squares programming solver. In CDC, pages 741-746. IEEE, 2002. URL: https://doi.org/10.1109/CDC.2002.1184594.
  55. Shmuel Safra. On the complexity of omega-automata. In FOCS, pages 319-327. IEEE Computer Society, 1988. URL: https://doi.org/10.1109/SFCS.1988.21948.
  56. Sriram Sankaranarayanan, Xin Chen, and Erika Ábrahám. Lyapunov Function Synthesis Using Handelman Representations. IFAC Proceedings Volumes, 46(23):576-581, 2013. URL: https://doi.org/10.3182/20130904-3-FR-2041.00198.
  57. Sriram Sankaranarayanan, Henny B. Sipma, and Zohar Manna. Constraint-based linear-relations analysis. In SAS, volume 3148 of Lecture Notes in Computer Science, pages 53-68. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-27864-1_7.
  58. Zhikun She, Haoyang Li, Bai Xue, Zhiming Zheng, and Bican Xia. Discovering Polynomial Lyapunov Functions for Continuous Dynamical Systems. Journal of Symbolic Computation, 58:41-63, November 2013. URL: https://doi.org/10.1016/J.JSC.2013.06.003.
  59. Richard S. Sutton and Andrew G. Barto. Reinforcement learning - an introduction. Adaptive computation and machine learning. MIT Press, 1998. Google Scholar
  60. Toru Takisaka, Yuichiro Oyabu, Natsuki Urabe, and Ichiro Hasuo. Ranking and repulsing supermartingales for reachability in randomized programs. ACM Trans. Program. Lang. Syst., 43(2):5:1-5:46, 2021. URL: https://doi.org/10.1145/3450967.
  61. Ðorđe Žikelić, Bor-Yuh Evan Chang, Pauline Bolignano, and Franco Raimondi. Differential cost analysis with simultaneous potentials and anti-potentials. In PLDI, pages 442-457. ACM, 2022. URL: https://doi.org/10.1145/3519939.3523435.
  62. Ðorđe Žikelić, Mathias Lechner, Thomas A. Henzinger, and Krishnendu Chatterjee. Learning control policies for stochastic systems with reach-avoid guarantees. In AAAI, pages 11926-11935. AAAI Press, 2023. URL: https://doi.org/10.1609/AAAI.V37I10.26407.
  63. Ðorđe Žikelić, Mathias Lechner, Abhinav Verma, Krishnendu Chatterjee, and Thomas A. Henzinger. Compositional policy learning in stochastic control systems with formal guarantees. In NeurIPS, 2023. Google Scholar
  64. Peixin Wang, Tengshun Yang, Hongfei Fu, Guanyan Li, and C.-H. Luke Ong. Static posterior inference of bayesian probabilistic programming via polynomial solving. Proc. ACM Program. Lang., 8(PLDI):1361-1386, 2024. URL: https://doi.org/10.1145/3656432.
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