Sound and Complete Proof Rules for Probabilistic Termination

on YouTube ↗19m

" summary

Presents sound and relatively complete proof rules for qualitative and quantitative termination of imperative programs with discrete probabilistic choice and demonic bounded nondeterminism (no sampling, rational variables). Shows how to construct supermartingale+variant construction from any almost‑surely terminating program, proves completeness by bounding escape probabilities, exposes a counterexample to a 2022 quantitative completeness claim, and gives an explicit almost‑sure termination proof for the two‑dimensional random walker.

AI-written summary · about

" chapters (10)

1. 0:00Introduction
2. 1:12Program model and termination
3. 3:41Proof rules for probabilistic termination
4. 6:09Deriving qualitative proof rule
5. 8:40Limitations of variant rule
6. 10:05Introducing supermartingales
7. 12:33Supermartingales and termination
8. 14:19Combining variants and supermartingales
9. 15:47Summary
10. 16:34Q&A