Document Open Access Logo

Deciding Termination of Simple Randomized Loops

Authors Éléanore Meyer , Jürgen Giesl

PDF

File

Thumbnail PDF
PDF
LIPIcs.MFCS.2025.76.pdf
  • Filesize: 1 MB
  • 19 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Probabilistic computation
  • Theory of computation → Program analysis
Keywords
  • decision procedures
  • randomized programs
  • linear loops
  • positive almost sure termination

Metrics

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

Abstract

We show that universal positive almost sure termination (UPAST) is decidable for a class of simple randomized programs, i.e., it is decidable whether the expected runtime of such a program is finite for all inputs. Our class contains all programs that consist of a single loop, with a linear loop guard and a loop body composed of two linear commuting and diagonalizable updates. In each iteration of the loop, the update to be carried out is picked at random, according to a fixed probability. We show the decidability of UPAST for this class of programs, where the program’s variables and inputs may range over various sub-semirings of the real numbers. In this way, we extend a line of research initiated by Tiwari in 2004 into the realm of randomized programs.

Cite As Get BibTex

Éléanore Meyer and Jürgen Giesl. Deciding Termination of Simple Randomized Loops. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 76:1-76:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.MFCS.2025.76

Author Details

Éléanore Meyer
  • RWTH Aachen University, Germany
Jürgen Giesl
  • RWTH Aachen University, Germany

Funding

DFG Research Training Group 2236 UnRAVeL.

Acknowledgements

We thank Sophia Greiwe for her help with the implementation of our decision procedure in SiRop.

Supplementary Materials

References

  1. 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.
  2. Robert B. Ash and Catherine A. Doléans-Dade. Probability and Measure Theory. Academic Press, 2nd ed. edition, 2000. Google Scholar
  3. Martin Avanzini, Georg Moser, and Michael Schaper. A modular cost analysis for probabilistic programs. Proc. ACM Program. Lang., 4(OOPSLA), 2020. URL: https://doi.org/10.1145/3428240.
  4. Ezio Bartocci, Laura Kovács, and Miroslav Stankovic. Automatic generation of moment-based invariants for prob-solvable loops. In Proc. ATVA '19, LNCS 11781, pages 255-276, 2019. URL: https://doi.org/10.1007/978-3-030-31784-3_15.
  5. 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 Proc. TACAS '23, LNCS 13994, pages 410-429, 2023. URL: https://doi.org/10.1007/978-3-031-30820-8_25.
  6. Olivier Bournez and Florent Garnier. Proving positive almost-sure termination. In Proc. RTA '05, LNCS 3467, pages 323-337, 2005. URL: https://doi.org/10.1007/978-3-540-32033-3_24.
  7. Mark Braverman. Termination of integer linear programs. In Proc. CAV '06, LNCS 4144, pages 372-385, 2006. URL: https://doi.org/10.1007/11817963_34.
  8. Tomás Brázdil, Krishnendu Chatterjee, Antonín Kucera, Petr Novotný, and Dominik Velan. Deciding fast termination for probabilistic VASS with nondeterminism. In Proc. ATVA '19, LNCS 11781, pages 462-478, 2019. URL: https://doi.org/10.1007/978-3-030-31784-3_27.
  9. Aleksandar Chakarov and Sriram Sankaranarayanan. Probabilistic program analysis with martingales. In Proc. CAV '13, LNCS 8044, pages 511-526, 2013. URL: https://doi.org/10.1007/978-3-642-39799-8_34.
  10. Krishnendu Chatterjee, Hongfei Fu, and Amir Kafshdar Goharshady. Termination analysis of probabilistic programs through positivstellensatz’s. In Proc. CAV '16, LNCS 9779, pages 3-22, 2016. URL: https://doi.org/10.1007/978-3-319-41528-4_1.
  11. Florian Corzilius, Gereon Kremer, Sebastian Junges, Stefan Schupp, and Erika Ábrahám. SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving. In Proc. SAT '15, LNCS 9340, pages 360-368, 2015. URL: https://doi.org/10.1007/978-3-319-24318-4_26.
  12. Florian Frohn and Jürgen Giesl. Termination of triangular integer loops is decidable. In Proc. CAV '19, LNCS 11562, pages 426-444, 2019. URL: https://doi.org/10.1007/978-3-030-25543-5_24.
  13. Jürgen Giesl, Peter Giesl, and Marcel Hark. Computing expected runtimes for constant probability programs. In Proc. CADE '19, LNCS 11716, pages 269-286, 2019. URL: https://doi.org/10.1007/978-3-030-29436-6_16.
  14. Jürgen Giesl, Albert Rubio, Christian Sternagel, Johannes Waldmann, and Akihisa Yamada. The termination and complexity competition. In Proc. TACAS '19, LNCS 11429, pages 156-166, 2019. Website of the Annual Termination Competition: https://termination-portal.org/wiki/Termination_Competition. URL: https://doi.org/10.1007/978-3-030-17502-3_10.
  15. Marcel Hark, Florian Frohn, and Jürgen Giesl. Polynomial loops: Beyond termination. In Proc. LPAR '20, EPiC 73, pages 279-297, 2020. URL: https://doi.org/10.29007/nxv1.
  16. Marcel Hark, Florian Frohn, and Jürgen Giesl. Termination of triangular polynomial loops. Formal Methods in Syst. Des., 65(1), 2025. URL: https://doi.org/10.1007/s10703-023-00440-z.
  17. Roger A. Horn and Charles R. Johnson. Matrix Analysis. Cambridge University Press, 2 edition, 2012. URL: https://doi.org/10.1017/CBO9781139020411.
  18. Mehran Hosseini, Joël Ouaknine, and James Worrell. Termination of linear loops over the integers. In Proc. ICALP '19, LIPIcs 132, 2019. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.118.
  19. Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. On the hardness of analyzing probabilistic programs. Acta Informatica, 56(3):255-285, 2019. URL: https://doi.org/10.1007/S00236-018-0321-1.
  20. Leonid Khachiyan and Lorant Porkolab. Computing integral points in convex semi-algebraic sets. In Proc. FOCS '97, pages 162-171, 1997. URL: https://doi.org/10.1109/SFCS.1997.646105.
  21. Andrey Kofnov, Marcel Moosbrugger, Miroslav Stankovic, Ezio Bartocci, and Efstathia Bura. Exact and approximate moment derivation for probabilistic loops with non-polynomial assignments. ACM Trans. Model. Comput. Simul., 34(3):18:1-18:25, 2024. URL: https://doi.org/10.1145/3641545.
  22. Nils Lommen and Jürgen Giesl. Targeting completeness: Using closed forms for size bounds of integer programs. In Proc. FroCoS '23, LNCS 14279, pages 3-22, 2023. URL: https://doi.org/10.1007/978-3-031-43369-6_1.
  23. Nils Lommen, Fabian Meyer, and Jürgen Giesl. Automatic complexity analysis of integer programs via triangular weakly non-linear loops. In Proc. IJCAR '22, LNCS 13385, pages 734-754, 2022. URL: https://doi.org/10.1007/978-3-031-10769-6_43.
  24. Éléanore Meyer, Jürgen Giesl, and Sophia Greiwe. SiRop. Software, DFG-Research Training Group 2236 UnRAVeL, (visited on 2025-08-05). URL: https://github.com/aprove-developers/SiRop
    Software Heritage Logo archived version
    full metadata available at: https://doi.org/10.4230/artifacts.24333
  25. Fabian Meyer, Marcel Hark, and Jürgen Giesl. Inferring expected runtimes of probabilistic integer programs using expected sizes. In Proc. TACAS '21, LNCS 12651, pages 250-269, 2021. URL: https://doi.org/10.1007/978-3-030-72016-2_14.
  26. Éléanore Meyer and Jürgen Giesl. Deciding termination of simple randomized loops, 2025. URL: https://doi.org/10.48550/arXiv.2506.18541.
  27. Marcel Moosbrugger, Ezio Bartocci, Joost-Pieter Katoen, and Laura Kovács. The probabilistic termination tool Amber. Formal Methods Syst. Des., 61(1):90-109, 2022. URL: https://doi.org/10.1007/S10703-023-00424-Z.
  28. 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.
  29. Saradha Natarajan and Ravindranathan Thangadurai. Pillars of Transcendental Number Theory. Springer, 2020. URL: https://doi.org/10.1007/978-981-15-4155-1.
  30. Van Chan Ngo, Quentin Carbonneaux, and Jan Hoffmann. Bounded expectations: Resource analysis for probabilistic programs. In Proc. PLDI '18, pages 496-512, 2018. URL: https://doi.org/10.1145/3192366.3192394.
  31. Joël Ouaknine, João Sousa Pinto, and James Worrell. On termination of integer linear loops. In Proc. SODA '15, pages 957-969, 2015. URL: https://doi.org/10.1137/1.9781611973730.65.
  32. Enric Rodríguez-Carbonell and Deepak Kapur. Automatic generation of polynomial loop invariants: Algebraic foundations. In Proc. ISSAC '04, pages 266-273, 2004. URL: https://doi.org/10.1145/1005285.1005324.
  33. SageMath, the Sage Mathematics Software System (Version 10.3), 2024. URL: https://www.sagemath.org.
  34. Nasser Saheb-Djahromi. Probabilistic LCF. In Proc. MFCS '78, LNCS 64, pages 442-451, 1978. URL: https://doi.org/10.1007/3-540-08921-7_92.
  35. Ashish Tiwari. Termination of linear programs. In Proc. CAV '04, LNCS 3114, pages 70-82, 2004. URL: https://doi.org/10.1007/978-3-540-27813-9_6.
  36. Di Wang, David M. Kahn, and Jan Hoffmann. Raising expectations: Automating expected cost analysis with types. Proc. ACM Program. Lang., 4(ICFP), 2020. URL: https://doi.org/10.1145/3408992.
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