This website uses technically necessary cookies to offer the best possible functionality.

Skip to Content Skip to Main Navigation Skip to Search

UnRAVeL – UNcertainty and Randomness in Algorithms, VErification and Logic

Talk: Proving Almost-Sure Termination With Non-Ranking Super Martingales

Wednesday, 15.11.2017, 11:00am

Location: RWTH Aachen University, Department of Computer Science - Ahornstr. 55, building E3, room 9u10

Speaker: Benjamin Kaminski

We present a super-martingale based proof method for proving almost-sure termination of probabilistic programs. The method is quite general and can prove almost-sure termination of programs even if the expected termination time is infinite. The almost-sure termination proofs in this setting tend to be quite simple, even for interesting examples. For example, it can prove almost-sure termination of a symmetric random walk by means of a very simple witness.

last updated : 30/07/2018