A Formal Verification Framework for Cooperative Multi-Agent Systems

Rational Verification is the problem of checking temporal logic properties of multi-agent systems modelled as multi-player games. Typically, in rational verification, we want to check whether a temporal logic formula is, or is not, satisfied on some or all equilibria of the game, assuming non-cooperative behaviour, for instance, as given by the Nash equilibria of the game. In this project, we want to investigate solutions to the rational verification problem but in cooperative multi-agent settings, where the stable behaviour of the system will be given by game-theoretic cooperative solution concepts, such as the core.