Skip to main content
Department of Information Technology

On Probabilistic Termination

Speaker:
Joost-Pieter Katoen, RWTH Aachen University

Date and Time
June 12 2019, 15:15 - 16:00

Location
Polacksbacken, ITC 1211.

Abstract
Program termination is a key question in program verification.
This talk considers the termination of probabilistic programs. These
programs describe randomised algorithms and receive recent attention in
machine learning.

Probabilistic termination has unexpected effects. For ordinary programs,
a program either terminates or not, terminating programs have a finite
run time, and termination in finite time is compositional: if P and Q
both terminate in finite time, P;Q does so too. These facts no longer
hold in the probabilistic setting.

Probabilistic programs may diverge with zero probability; this is called
almost-surely termination (AST). Running two AST-programs in sequence
that both have a finite expected termination time -- so-called positive
AST -- may yield an AST-program with an infinite termination time (in
expectation). Thus positive AST is not compositional with respect to
sequential program composition.

We show that proving positive AST (and AST) is "more undecidable" than
the halting problem, present a powerful proof rule for deciding AST, and
sketch a Dijkstra-like weakest precondition calculus for proving
positive AST in a compositional manner by reasoning at the syntax level.

Back to the seminar page

Updated  2019-05-27 12:44:50 by Philipp Rümmer.