Group colloquium: How to prove that a program almost surely terminate?

When: March 29, 2018, 15:45-16:45

Where: RA 3336

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.

	Home > News and Events > Events
<< EEMCS (EWI) Home News and Events » Group Colloquium » Events » In the Media People Research Education Vacancies Intranet Contact	Group colloquium: How to prove that a program almost surely terminate? When: March 29, 2018, 15:45-16:45 Where: RA 3336 Who: Joost-Pieter Katoen 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.