*

*

*                          Einladung

*

*

*

*                     Informatik-Oberseminar

*

*

*

+**********************************************************************

Zeit:  Freitag, 8. Februar 2019, 14:00 Uhr

Ort:   Raum 9222, E3, Ahornstr. 55

Referent: Benjamin Kaminski, M.Sc.

          Lehrstuhl für Informatik 2

Thema: Advanced Weakest Precondition Calculi for Probabilistic Programs

Abstract:

We study quantitative reasoning about probabilistic programs. In doing so, we investigate two main aspects: The reasoning techniques themselves and the computational hardness of that reasoning.

As for the former aspect, we first give an introduction to weakest preexpectation reasoning à la McIver & Morgan - a reasoning technique for the verification of probabilistic programs that builds on Dijkstra's weakest precondition calculus for programs with nondeterminism and Kozen's probabilistic propositional dynamic logic for probabilistic programs. We then present advanced weakest-preexpectation-style calculi for probabilistic programs that enable reasoning about

 - expected runtimes,

 - conditional expected values and conditional probabilities, and

 - expected values of mixed-sign random variables.

As with Dijkstra's calculus, our calculi are defined inductively on the program structure and thus allow for compositional reasoning on source code level. We put a special emphasis on proof rules for reasoning about loops.

The second aspect we study is the inherent computational hardness of reasoning about probabilistic programs, which is independent from the employed analysis technique. In particular, we study the hardness of approximating expected values and (co)variances as well as the hardness of deciding termination of probabilistic programs. While we study different notions of probabilistic termination, for instance almost-sure termination or termination within finite expected time (also known as positive almost-sure termination), we demonstrate that deciding termination of probabilistic programs is generally strictly harder than deciding termination of nonprobabilistic programs.

Es laden ein: die Dozentinnen und Dozenten der Informatik