Skip to main content

A Formal Verification Framework for Cooperative Multi-Agent Systems

Primary supervisor

Julian Gutierrez Santiago

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.

Student cohort

Double Semester

Required knowledge

The student should have strong mathematical skills, and ideally some knowledge of computational complexity, automata theory, and basics of logic and proof.