Verification and Control of Stochastic Multi-agent Systems
Probabilistic model checking provides a powerful set of techniques for automated formal verification of computerised systems operating in uncertain environments. Extensions of these methods to multi-agent systems open up the possibility to formally model and analyse systems with multiple components or actors, potentially acting in either an adversarial or collaborative manner.
This talk surveys some recent advances in this area, bringing together techniques and tools from formal verification with game-theoretic concepts and methods, notably stochastic games and equilibria.
We illustrate applications of this approach to component-based design and analysis in a variety of application domains, from multi-robot control to distributed protocols for network communication or energy management. We also discuss some of the key challenges and research directions to make further progress in the area.