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.