Model Checking and Strategy Synthesis for Stochastic Games: From Theory to Practice
summary
Extension of PRISM implements turn-based stochastic multiplayer games and a temporal logic called RP-ATL to specify probabilistic and reward objectives and to synthesize strategies. PRISM Games 2.0 produces Pareto curves for multi-objective trade-offs and returns randomized strategies when needed, sometimes requiring infinite memory; value iteration and compositional assume–guarantee synthesis speed analysis. Examples include aiming for safety probabilities like 10^-5, explicit-state implementation with a symbolic backend in progress, and open gaps in perception, partial observability, trust and ethics.
AI-written summary · about
chapters (29)
- 0:00Intro
- 3:03Are we safe?
- 3:58Software everywhere
- 4:54Quantitative verification
- 5:52Quantitative/probabilistic verification
- 7:27Historical perspective
- 8:15But which modelling abstraction?
- 9:23The challenge of mobile autonomy
- 10:45What makes a game?
- 11:50Playing games with the Google car...
- 12:19This lecture...
- 13:27Stochastic multi-player games (SMGs)
- 15:59Rewards
- 17:18Paths, strategies + probabilities
- 19:45Property specification: PATL
- 21:59PATL reward properties
- 23:28Examples
- 24:31Verification and strategy synthesis
- 25:54Value iteration
- 26:09Multi-objective properties
- 27:35Example of Pareto optimality
- 30:07Multidimentional Pareto set
- 30:32Compositional strategy synthesis
- 32:49Tool support: PRISM-games 2.0
- 33:14Case studies
- 33:36Summary so far...
- 35:45Perception software
- 37:41Conclusion
- 39:19Acknowledgements
related talks
17mProgrammatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Progr...
14mSequential Monte Carlo Program Synthesis with Refinement Proposals
20mThe Complexity of Infinite-Horizon General-Sum Stochastic Games
16mA Model-Driven Generative Self Play-Based Toolchain for Developing Games and Players
15mMulti-Agent Reinforcement Learning In Stochastic Games: From Alphago To Robust Control
04m1-2-3-Go! Policy Synthesis for Parameterized Markov Decision Processes via(…)
32mProbabilistic and Differentiable Programming in Scientific Simulators
55mLearning Safe Action Models