Multi-Agent Verification and Control with Probabilistic Model Checking

Probabilistic model checking builds upon ideas and techniques from a
diverse range of fields, from logic, automata and graph theory, to
optimisation, numerical methods and control. In recent years, it has
also been extended to integrate ideas from game theory, notably using
models such as stochastic games and solution concepts such as
equilibria, to formally verify the interaction of multiple rational
agents with distinct objectives. This provides a means to reason
flexibly about agents acting in either an adversarial or a collaborative
fashion, and opens up opportunities to tackle new problems within, for
example, artificial intelligence, robotics and autonomous systems. This
talk will summarise some of the advances in this area, and highlight
applications for which the techniques have already been used. It will
discuss how the strengths of probabilistic model checking apply, or have
the potential to apply, to the multi-agent setting and outline some of
the key challenges required to make further progress in this field.