Lecture
This lecture covers the formal analysis of stochastic systems, focusing on martingales and their applications in probabilistic programs, stochastic control, and quantitative termination analysis. It explores the concept of martingales as stochastic processes constant or decreasing in expectation, with examples like Gambler's ruin. The talk delves into stochastic invariants, supermartingales, and their role in certifying termination probabilities. It also discusses the completeness of stochastic invariants for quantitative termination analysis and the synthesis of certificates for termination. The lecture concludes with a discussion on stability verification and control in stochastic systems, including the use of neural network supermartingales. Future work includes improving algorithms for better bounds and conditioning.