Model checking of stochastic games
Supervisor
Suitable for
Abstract
This project will develop formal verification techniques for stochastic games, in particular by considering techniques based
on game-theoretic notions of equilibria. A range of such techniques are already implemented in the PRISM-games model checker.
This project will consider extensions of these approaches to tackling new types of equilibria, such as Stackelberg equilibria,
with potential directions including designing extended temporal logics and solution methods, or modelling new applications,
for example from multi-robot coordination.
