2026-09-20T14:11:24Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:24183 2026-09-05T18:35:51Z ddc:004 open_access

Deciding Termination of Simple Randomized Loops Meyer, Éléanore Giesl, Jürgen decision procedures randomized programs linear loops positive almost sure termination 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Éléanore Meyer and Jürgen Giesl 2025 Is Part Of LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.MFCS.2025.76 urn:nbn:de:0030-drops-241833 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.76 eng https://creativecommons.org/licenses/by/4.0/legalcode