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.