Termination of probabilistic programs

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.

The Online Worldwide Seminar on Logic and Semantics is a new series of fortnightly 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.

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:

Virtual “coffee breaks” before and after the seminar, allowing participants to chat in small groups, replicating the social element of a real-world conference. Robust technology platform supporting hundreds of interactive participants. Live-stream of the speaker’s slides visible alongside the speaker’s face, allowing nuanced communication at a human level. Chairperson to introduce the speaker, facilitate questions from the audience, and keep proceedings running on time. Aggregate nonverbal feedback from audience members, such as “go faster” or “slow down”, reported in real-time to the speaker. Audience members whose question is selected by the chairperson can deliver it in full audio and video, giving a natural interaction with the speaker. No need to register, just show up.

This talk is hosted by University of Birmingham. Link to the talk site.