Automating termination analysis of probabilistic programs

Abstract

Deciding termination of computer programs is one of the most infamous challenges in computer science. In this thesis, we automate the termination analysis of a class of probabilistic programs, called Prob-solvable loops, through (super-)martingale based proof rules. We establish incomplete but sound algorithms for almost-sure termination, positive-almost-sure termination, and the negations thereof. We achieve this, by exploiting the structural restrictions of Prob-solvable loops. The restrictions let us effectively compute asymptotic bounds on polynomial expressions of program variables. These bounds are then used to decide the preconditions of the probabilistic termination proof rules, like the supermartingale condition. For certifying the negation of almost-sure termination, we generalize existing proof rules involving repulsing supermartingales, to handle unbounded polynomial variable updates of programs. This generalization applies to general probabilistic programs even beyond Prob-solvable loops. Moreover, we identify a subclass of probabilistic programs and introduce a sound and complete procedure deciding almost-sure termination of such programs. Our identified subclass strictly subsumes the class of so-called constant probability programs, the largest decidable subclass currently known. We combine our proposed algorithms for probabilistic termination analysis in our new tool Amber. Experimental results demonstrate that Amber can handle probabilistic programs that are out of reach for other state-of-the-art tools.

Die Terminierung von Computerprogrammen zu entscheiden ist eines der ersten und berüchtigtsten Probleme der Informatik. In dieser Arbeit automatisieren wir die Terminierungsanalyse einer Klasse von probabilistischen Programmen, der Klasse sogenannter Prob-solvable loops, mithilfe von Beweisregeln basierend auf Supermartingalen. Wir konstruieren Algorithmen für almost-sure-termination, positive-almost-sure-termination, sowie für die Negationen der Konzepte. Für diesen Zweck nutzen wir strukturelle Eigenschaften von Prob-solvable loops. Die Eigenschaften ermöglichen uns asymptotische Schranken für polynomielle Ausdrücke über Programmvariablen automatisch zu berechnen. Diese Schranken werden dann benutzt, um die Bedingungen der probabilistischen Beweisregeln, wie zum Beispiel die Bedingung für Supermartingale, zu überprüfen. Um die Negation von almost-sure-termination festzustellen, verallgemeinern wir existierende Beweisregeln, die auf repulsiven Supermartingalen basieren. Dies ermöglicht uns unbeschränkte, polynomielle Updates von Programmvariablen zu unterstützen. Die verallgemeinerte Beweisregel ist für allgemeine probabilistische Programme verwendbar und nicht nur für Prob-solvable loops. Weiters, identifizieren wir eine Subklasse von probabilistischen Programmen, für die wir einen vollständigen und korrekten Algorithmus entwickeln, welcher almost-sure-termination für Programme der Subklasse entscheidet. Unsere identifizierte Subklasse ist strikt größer als die Klasse sogenannter constant-probability-programs, welches die größte derzeit bekannte Klasse ist, für die almost-sure-termination entscheidbar ist. Wir kombinieren die entwickelten Algorithmen für die probabilistische Terminierungsanalyse in unserem neuen Softwaretool Amber. Experimentelle Ergebnisse zeigen, dass Amber probabilistische Programme handhaben kann, die unerreichbar für andere state-of-the-art Tools sind.