Towards complete methods for automatic complexity and termination analysis of (probabilistic) programs

Hark, Marcel Tobias; Kovács, Laura; Giesl, Jürgen

doi:HT020974236

Towards complete methods for automatic complexity and termination analysis of (probabilistic) programs = Methoden für die automatische Komplexitäts- und Terminierungsanalyse von (probabilistischen) Programmen und ihre Vollständigkeit

Hark, Marcel Tobias^RWTH*

2021

Verantwortlichkeitsangabevorgelegt von Marcel Hark, Master of Science

ImpressumAachen : RWTH Aachen University 2021

Umfang1 Online-Ressource : Illustrationen

Dissertation, RWTH Aachen University, 2021

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Giesl, Jürgen (Thesis advisor)^RWTH* ; Kovács, Laura (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2021-06-18

Online
DOI: 10.18154/RWTH-2021-06073
URL: https://publications.rwth-aachen.de/record/821181/files/821181.pdf

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
completeness (frei) ; expected runtime (frei) ; formal verification (frei) ; polynomial loops (frei) ; probabilistic programs (frei) ; runtime complexity (frei) ; termination analysis (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
Die steigende Zahl von Computerprogrammen in unserem Alltag hat zu immer umfangreicheren Softwaresystemen geführt. Die klassische Herangehensweise, um die Korrektheit solcher Systeme zu garantieren, ist formale Verifikation. Zwei der wichtigsten Eigenschaften von Programmen sind Terminierung und Effizienz. Außerdem wird in den letzten Jahren Randomisierung in der Programmierung immer wichtiger. So haben probabilistische Konzepte sich als sehr erfolgreich erwiesen, um Systeme aus praxisnahen Anwendungen zu modellieren. Diese Dissertation untersucht die formale Verifikation von Programmen, welche auch randomisierte Zuweisungen durch diskrete Zufallsverteilungen unterstützen. Hierbei sind wir besonders daran interessiert, Terminierung bzw. Nichtterminierung zu beweisen und Schranken für die (erwartete) Laufzeit zu berechnen. Verifikation von Programmen ist im Allgemeinen unentscheidbar. Dennoch sind wann immer möglich vollständige Ansätze zur Verifikation bestimmter Eigenschaften von (Teil-)Klassen von Programmen unvollständigen vorzuziehen, da sie immer ein eindeutiges Ergebnis liefern, also entweder einen Beweis oder ein Gegenbeispiel. Ein wichtiges Ziel dieser Arbeit ist daher die Charakterisierung von Teilklassen von Programmen, für die vollständige Techniken zur Analyse von Terminierung und Laufzeitkomplexität existieren. Um Systeme zu analysieren, die aus praxisnahen Anwendungen hervorgehen, muss formale Verifikation automatisch ablaufen. Daher studieren wir auch die Automatisierung der hier vorgestellten Techniken. Die Beiträge dieser Arbeit sind im Folgenden aufgelistet. (1) Wir beschreiben Klassen nicht-probabilistischer Programme, für die sowohl Terminierung auf einer gegebenen Eingabe als auch Terminierung auf allen Eingaben entscheidbar sind, nichtterminierende Eingaben rekursiv aufgezählt und obere Schranken für die Laufzeit immer berechnet werden können. (2) Wir verknüpfen die Semantik probabilistischer Programme, die durch sogenannte Erwartungs-Kalküle gegeben ist, mit jener, die durch sogenannte stochastische Prozesse definiert ist. So erhalten wir die ersten induktiven Beweisregeln zur Bestimmung unterer Schranken für die erwarteten Ausgaben bzw. Laufzeiten probabilistischer Programme. (3) Wir präsentieren eine Klasse probabilistischer Programme, für welche nicht nur Terminierung entscheidbar ist und sowohl obere als auch untere Schranken für die erwartete Laufzeit leicht hergeleitet werden können, sondern auch eine geschlossene Form für die exakte erwartete Laufzeit immer berechnet werden kann. (4) Wir entwickeln einen Ansatz zur Bestimmung oberer Schranken für die erwartete Laufzeit allgemeiner probabilistischer Programme. Hierfür benutzen wir sowohl Schranken für die klassische Laufzeit bzw. Größe von Variablenwerten als auch eine abwechselnde Berechnung von Schranken für die erwartete Laufzeit bzw. Größe. Unsere experimentelle Auswertung zeigt die große Leistungsfähigkeit dieses Ansatzes.

The increasing importance of computer programs in our everyday life has led to more and more complex software systems. To prove correctness of such a system, formal verification is the standard methodology. Two of the most important properties of a program are its termination behavior and its efficiency. Moreover, in recent years randomization in programming has gained a lot of interest. For example, to model non-deterministic behavior in real-world applications, probabilistic concepts have proved very successful. In this thesis, we investigate formal verification of programs which also feature assignments via discrete probability distributions. In particular, we are interested in proving (non-)termination and inferring bounds on the (expected) worst-case runtime of such programs. In general, formal verification of programs is undecidable. Still, whenever possible, complete approaches for verifying certain properties on (sub-)classes of programs are preferable to incomplete ones since they always yield definite results, i.e., either a proof or a counterexample. Hence, we characterize sub-classes of programs for which we can present complete approaches for analyzing termination and runtime complexity. To analyze systems arising from real-world applications, formal verification has to proceed automatically. Thus, we also investigate the automation of our results.The contributions of this thesis are as follows: (1) We characterize classes of non-probabilistic programs where both termination on a single input as well as all inputs are decidable, witnesses for non-termination are recursively enumerable, and upper bounds on the runtime can always be computed. (2) We connect the semantics of probabilistic programs that is defined via so-called expectation transformers to the semantics defined via so-called stochastic processes.This leads to the first inductive proof rules for lower bounds on expected outcomes and expected runtimes of probabilistic programs. (3) We present a class of probabilistic programs where not only probabilistic termination is decidable and both upper and lower bounds on the expected runtime can easily be inferred but also a closed form for the exact expected runtime can always be computed. (4) We develop an approach for deriving upper bounds on the expected runtime of general probabilistic programs. To this end, we use non-probabilistic runtime and size bounds as well as an alternating computation of expected runtime and size bounds. Our experiments demonstrate the performance and the applicability of this approach.

OpenAccess:
PDF
(additional files)