Verification with Stochastic Games: Advances and Challenges

---

Modern computing systems increasingly involve autonomous agents acting concurrently, often either competing or collaborating to achieve differing objectives. Game-theoretic approaches offer a natural way to reason about the subtle behaviour of these systems. A further challenge is the need for probabilistic modelling: consider a multi-robot team operating in a noisy, uncertain environment, or a distributed network protocol employing randomisation. For these cases, stochastic games are a powerful modelling formalism. But until recently practical tools and techniques for formal verification using these models have been lacking.

In this talk, we summarise the development of techniques for formal verification using stochastic games, and the associated model checking tool PRISM-games. We express quantitative correctness properties in temporal logic, and automatically synthesise strategies for agents which provide probabilistic guarantees on their correct behaviour. We describe recent advances in this area, including the use of concurrent stochastic games, for more realistic modelling of agents interacting concurrently, and Nash equilibria, for modelling multiple distinct agent objectives. We illustrate these techniques with examples from a range of applications, and also identify some of the future challenges that exist in the area.