Primary supervisorJulian Gutierrez Santiago
Model checking is an automated formal verification technique in which, given a property F – typically represented as a temporal logic formula – and a model of a system M, one checks whether the system M satisfies property F. Model checking is a well understood formal verification technique supported by several tools, many of which are available online. A little less is known about probabilistic model checking. In this setting, M is a model containing probabilistic behaviour; for instance, M may be a Markov Decision Process (MDP) modelling the behaviour of an AI system, for instance as in Reinforcement Learning (RL). In this case, instead of checking whether F is or is not satisfied by M, one is interested in computing the probability that F is satisfied on M. The goal of this project is to write a program that model checks an MDP M against a temporal logic formula F in systems consisting of multiple AI agents modelled as Probabilistic Multi-Agent Systems (MAS). Part of the project is to learn about the state-of-the-art algorithms to do probabilistic model checking, and based on that knowledge, to explore ways to check that a property can be satisfied with probability 1 for a number of different temporal logic languages.
The student should have strong mathematical skills, and ideally some knowledge of computational complexity, automata theory, and basics of logic and proof.