Skip to main content

Primary supervisor

Julian 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.

Student cohort

Single 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.