Termination of probabilistic programs

Joost-Pieter Katoen (RWTH Aachen University)

15-Apr-2020, 13:00-14:00 (4 years ago)

Abstract: Program termination is a key question in program verification. This talk considers the termination of probabilistic programs, programs that can describe randomised algorithms and more recently received attention in machine learning. Probabilistic termination has several nuances and has some unexpected effects. Programs may diverge with zero probability; they almost-surely terminate (AST). Two AST-programs run in sequence may have an infinite expected run-time, though each of its constituents has a finite expected run-time.

This talk will demystify the notions of probabilistic termination, its surprising effects, and its hardness ("degree of undecidability"). We will show a simple proof rule for deciding AST.

logic

Audience: researchers in the topic


Online Worldwide Seminar on Logic and Semantics (OWLS)

Series comments: The Online Worldwide Seminar on Logic and Semantics is a new series of research talks, highlighting the most exciting recent work in the international computer science logic community. The scope of the seminar series is roughly that of the major computer science logic conferences such as LICS, ICALP and FSCD. It takes place on most Wednesdays, with a focus every other week on the work of young researchers.

In this time of restricted international travel, a key aim of this series is to provide a forum for the informal discussion and social interaction that is so important for the progress of science. To facilitate this, the seminar incorporates in virtual form a number of features more normally associated with physical meetings.

For more details, please visit the homepage. There is no need to register for the talks, just show up.

Organizers: Alexandra Silva, Pawel Sobocinski, Jamie Vicary, Nathanaƫl Fijalkow, Charles Grellois, S. Krishna, Koko Muroya
Curator: Alakh Dhruv Chopra*
*contact for this listing

Export talk to