Deciding Termination of Simple Randomized Loops
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
@article{arxiv.2506.18541,
title = {Deciding Termination of Simple Randomized Loops},
author = {Éléanore Meyer and Jürgen Giesl},
journal= {arXiv preprint arXiv:2506.18541},
year = {2025}
}