Positive Almost-Sure Termination of Polynomial Random Walks

Abstract

Die Laufzeit eines probabilistischen Programmes ist eine Zufallsvariable. Termination solcher Programme umfasst deshalb den qualitativen Terminationsbegriff “almost-sure termination” (AST) sowie den quantitativen Begriff “positive almost-sure termination” (PAST), welcher eine Aussage über den Erwartungswert der Laufzeit trifft. Ein Programm welches im Sinne von PAST terminiert, terminiert auch im Sinne von AST, jedoch terminiert nicht jedes Programm, welches im Sinne von AST terminiert auch im Sinne von PAST. Der symmetrische Random Walk ist ein Beispiel für ein Programm, welches AST, aber nicht PAST erfüllt. In dieser Arbeit zeigen wir, dass die Klasse der “Polynomiellen Random Walks” unter bestimmten Umständen PAST erfüllt. In jedem Schleifendurchlauf wird mit einer konstanten Wahrscheinlichkeit p eines von zwei Polynomen in der Anzahl der bisherigen Schleifendurchläufen gewählt, welches die Größe und Richtung des nächsten Schrittes bestimmt. Wir zeigen, dass ein Programm PAST erfüllt, wenn der Grad der Polynome sowohl höher als der Grad des Erwartungswertes der Schritte ist, als auch einen gewissen Schwellenwert d_min(p) übersteigt. Unser Ansatz verwendet keine Beweisregeln und Arithmetische Ausdrücke wie Martingale oder Invarianten. Stattdessen beschränken wir den oberen Rand der Zufallsvariable, welche die Schritte akkumuliert, induktiv, und zeigen mit Hilfe dieser Beschränkung, dass PAST erfüllt sein muss. Weiters implementieren wir die Annäherung dieser Schranke mittels eines genetischen Algorithmus und linearer Optimierung.

The number of steps until termination of a probabilistic program is a random variable. Probabilistic program termination therefore requires qualitative analysis via almost-sure termination (AST), while also providing quantitative answers via positive almost-sure termination (PAST) on the expected number of steps until termination. While every program which is PAST is AST, the converse is not true. The symmetric random walk with constant step size is a prominent example of a program that is AST but not PAST. In this thesis we show that a more general class of polynomial random walks is PAST. Our random walks implement a step size that is polynomially increasing in the number of loop iterations and have a constant probability p of choosing either branch. We show that such programs are PAST when the degree of the polynomial is higher than both the degree of the drift and a threshold d_min(p). Our approach does not use proof rules, nor auxiliary arithmetic expressions, such as martingales or invariants. Rather, we establish an inductive bound for the cumulative distribution function of the loop guard, based on which PAST is proven. We implemented the approximation of this threshold, by combining genetic programming, algebraic reasoning and linear programming.