Lower Bounds for Possibly Divergent Probabilistic Programs

on YouTube ↗17m

" summary

A proof rule called guard strengthening gives sound lower bounds for weakest preexpectations of possibly divergent probabilistic loops by replacing loop guards with finite barriers, avoiding uniform integrability side conditions. The method proves nontrivial termination and expectation lower bounds, is tight as the barrier M → ∞, and is partially automated by building a finite-state model and running PRISM to extract numeric bounds (three‑dimensional random walk return prob ≈ ~0.34 and a Zeroconf example with barrier 10).

AI-written summary · about

" chapters (17)

1. 0:00Lower bounds for probabilistic programs
2. 0:44Random walks and termination
3. 1:46Probabilistic programs challenges
4. 2:50Weakest pre-expectations semantics
5. 4:33Weakest pre-expectations for loops
6. 5:38Upper bound techniques limits
7. 6:42Lower bounds and uniform integrability
8. 7:47God strengthening proof rule
9. 8:30God strengthening intuition
10. 10:14Purpose of the new rule
11. 11:16God strengthening properties
12. 12:21Rule tightness and precision
13. 12:41Automation with model checking
14. 13:44Example: 3D random walk
15. 14:05Example: ZeroConf protocol
16. 15:09Summary and conclusion
17. 15:54Q&A: Limitations