Termination Analysis of Probabilistic Programs with Martingales
Krishnendu Chatterjee, Hongfei Fu, Petr Novotný · Cambridge University Press eBooks · 2020
For non-probabilistic programs, a key question in static analysis is termination, which asks whether a given program terminates under a given initial condition. In the presence of probabilistic behaviour, there are two fundamental extensions of the termination question: (a) the almost-sure termination question, which asks whether the termination probability is 1; and (b) the bounded-time termination question, which asks whether the expected termination time is bounded. There are many active research directions to address these two questions; one important such direction is the use of martingale theory for termination analysis. In this chapter, we survey the main techniques of the martingale-based approach to the termination analysis of probabilistic programs.