Abstract : Software faults have plagued computing systems since the early days, leading to the development of methods based on mathematical logic, such as proof assistants or model checking, to ensure their correctness. The rise of AI calls for automated decision making that incorporates strategic reasoning and coordination of behaviour of multiple autonomous agents acting concurrently and in presence of uncertainty. Traditionally, game-theoretic solutions such as Nash equilibria are employed to analyse strategic interactions between multiple independent entities, but model checking tools for scenarios exhibiting concurrency, stochasticity and equilibria have been lacking.

This lecture will focus on a recent extension of probabilistic model checker PRISM-games (www.prismmodelchecker.org/games/), which supports quantitative reasoning and strategy synthesis for concurrent multiplayer stochastic games against temporal logic that can express coalitional, zero-sum and equilibria-based properties. Game-theoretic models arise naturally in the context of autonomous computing infrastructure, including user-centric networks, robotics and security. Using illustrative examples, this lecture will give an overview of recent progress in probabilistic model checking for stochastic games, including Nash and correlated equilibria, and highlight challenges and opportunities for the future.

Keywords : probability; model checking; games