Deciding Termination of Simple Randomized Loops

TL;DR

This paper proves that the universal positive almost sure termination problem is decidable for a specific class of simple randomized loops with linear guards and updates, extending previous research into randomized programs.

Contribution

It establishes the decidability of UPAST for programs with linear, commuting, and diagonalizable updates, broadening the scope of termination analysis for randomized loops.

Findings

Decidability of UPAST for the specified class of programs.

Extension of Tiwari's 2004 research to randomized programs.

Applicability to variables over various sub-semirings of the reals.

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.