Mar 29, 2018: Joost-Pieter Katoen: How to prove that a program almost surely terminate?

March 29, 2018How to prove that a program almost surely terminate?
Room: RA 3336Joost-Pieter Katoen
15:45-16:45

A key question for a probabilistic program is whether the probability
mass of all its diverging runs is zero, that is, that it terminates
"almost surely". Proving that is a notoriously hard problem, it is
Pi2-hard, to be precise. Whereas for ordinary programs a ranking (or
variant) function suffices to prove certain termination, this is no
longer the case for probabilistic programs.

In this talk, I'll present a new proof rule that allows for proving
almost-sure termination for a rich set of programs and give some simple,
though counter-intuitive examples of almost-surely terminating programs.