Semantics and loop invariant synthesis for probabilistic programs = Semantiken und Schleifeninvariantensynthese für probabilistische Programme

Gretz, Friedrich

2016

Verantwortlichkeitsangabevorgelegt von Friedrich Gretz

ImpressumAachen : Publikationsserver der RWTH Aachen University 2016

Aachen, Techn. Hochsch., Diss., 2015

Veröffentlicht auf dem Publikationsserver der RWTH Aachen University 2016

Genehmigende Fakultät
Fak01

Hauptberichter/Gutachter
Katoen, Joost-Pieter (Thesis advisor) ; Sankaranarayanan, Sriram (Thesis advisor)

Tag der mündlichen Prüfung/Habilitation
2015-09-25

Online
URN: urn:nbn:de:hbz:82-rwth-2015-067916
URL: http://publications.rwth-aachen.de/record/561346/files/561346.pdf
URL: http://publications.rwth-aachen.de/record/561346/files/561346.pdf?subformat=pdfa

Einrichtungen

Inhaltliche Beschreibung (Schlagwörter)
Informatik (frei) ; probabilistic programming (frei) ; Markov decision process (frei) ; expectation transformer semantics (frei) ; operational semantics (frei) ; expected rewards (frei) ; conditional probabilities (frei) ; program transformation (frei) ; probabilistic loop invariants (frei) ; invariant generation (frei)

Thematische Einordnung (Klassifikation)
DDC: 004

Kurzfassung
In dieser Arbeit beschäftigen wir uns mit sequentiellen probabilistischen Programmen.Derartige Programme dienen als Modell für randomisierte Algorithmenin der Informatik. Sie erlauben beispielsweise die formale Analyse von Effektivitätund Korrektheit von Algorithmen oder auch die Beurteilung von Sicherheitsaspektenin Protokollen. Wir entwickeln eine operationelle Semantik für probabilistische Programmeund zeigen, dass diese äquivalent zur Semantik nach McIver und Morgan ist,die auf Transformationen von Erwartungswerten basiert. Diese Äquivalenzbeziehungzweier Semantiken verschafft uns ein tiefer gehendes Verständnis fürdas Verhalten von probabilistischen Programmen. Weiterhin können nun Forschungsergebnisse, die auf Transitionssystemen wie zum Beispiel den Markow-Entscheidungsprozessen beruhen, in die Terminologie von deduktiven Verifikationsverfahren, beispielsweise Erwartungswerttransformationen, übersetzt werden – und umgekehrt.In einem weiteren Schritt fügen wir ein Sprachkonzept für Beobachtungenhinzu. Beide Semantiken können entsprechend erweitert werden und erlaubenes uns, bedingte Erwartungswerte zu ermitteln. Das heißt, wir berechnen beispielsweiseden erwarteten Wert einer Programmvariable unter der Bedingung,dass alle Beobachtungen während des Programmablaufs eingehalten werden. Unser Hauptaugenmerk richtet sich hierbei auf die auftretenden Schwierigkeiten imUmgang mit nicht terminierenden, nicht deterministischen oder undurchführbaren Programmen. Der Beitrag dieser Arbeit ist es auch solchen Programmen einewohl definierte Bedeutung zuzuordnen. Zusätzlich diskutieren wir Programmtransformationen,die es erlauben Beobachtungen aus den Programmen zu entfernen. Im letzten Teil dieser Arbeit gehen wir zur Verifikation von probabilistischen Programmen über. Dabei interessieren wir uns für die Automatisierung von induktivenÜberprüfungsmethoden. Wie üblich, stellen dabei Schleifen in Programmendas größte Hindernis dar, da sie die Berechnung von Fixpunkten oder dasAuffinden von induktiven Schleifeninvarianten erfordern. Während die Generierung von Schleifeninvarianten bereits für nicht probabilistische Programme einezentrale Herausforderung darstellt, wird diese Aufgabe in unserer Situation noch schwieriger, da sie eine quantitative Beweisführung verlangt. Als Lösungsansatzkonzentrieren wir uns auf ein Verfahren, das ausgehend von benutzerdefinierten Schablonen, quantitative Schleifeninvarianten generiert. Dieses Verfahren wirdals Software-Tool Prinsys implementiert und anhand von einigen Beispielen evaluiert.

In this thesis we consider sequential probabilistic programs. Such programsare a means to model randomised algorithms in computer science. They facilitatethe formal analysis of performance and correctness of algorithms or securityaspects of protocols.We develop an operational semantics for probabilistic programs and showit to be equivalent to the expectation transformer semantics due to McIver andMorgan. This connection between the two kinds of semantics provides a deeperunderstanding of the behaviour of probabilistic programs and is instrumental totransfer results between communities that use transition systems such as Markovdecision processes to reason about probabilistic behaviour and communities thatfocus on deductive verification techniques based on expectation transformers.As a next step, we add the concept of observations and extend both semanticsto facilitate the calculation of expectations which are conditioned on the fact thatno observation is violated during the program’s execution. Our main contributionhere is to explore issues that arise with non-terminating, non-deterministic or infeasibleprograms and provide semantics that are generally applicable. Additionally,we discuss several program transformations to facilitate the understandingof conditioning in probabilistic programming.In the last part of the thesis we turn our attention to the automated verificationof probabilistic programs. We are interested in automating inductive verificationtechniques. As usual the main obstacle in program analysis are loopswhich require either the calculation of fixed points or the generation of inductiveinvariants for their analysis. This task, which is already hard for standard, i.e.non-probabilistic, programs, becomes even more challenging as our reasoningbecomes quantitative. We focus on a technique to generate quantitative loop invariantsfrom user defined templates. This approach is implemented in a softwaretool called Prinsys and evaluated on several examples.

OpenAccess:
Download fulltext PDF PDF (PDFA)
(additional files)