Skip to main content

Algorithms for Parity Games

Primary supervisor

Julian Gutierrez Santiago

Parity games are a simple tool used in automated verification. They are played by two players on a finite labelled transition graph formally modelling a verification problem; for instance, that a model M of a computer system satisfies a given correctness property P. In such games, while one of the players (the Verifier) tries to show that M satisfies P, that is that M is a model of P, the other player (the Falsifier) tries to show otherwise. It is known that in these games there is always a memoryless winning strategy for one of the players – either for the Verifier if M is a model of P, or for the Falsifier if M is not. From a complexity point of view, parity games are known to be in both NP and co-NP, but not known to be solvable in polynomial time, which has attracted a lot of research into the topic. In fact, many algorithms have been developed to solve parity games, most of which have been implemented in PGSolver, a tool that has become in recent years the main platform to efficiently solve parity games. Motivated by the desire to find efficient solutions for parity games in practical settings, the goal of this project is to develop new algorithms to solve parity games, in particular, using SAT solving or constraint programming techniques, which tend to work quite well in practice, and to evaluate the performance of the new solutions against different PGSolver benchmarks.

Student cohort

Double Semester

Required knowledge

The student should have strong mathematical skills, and ideally some knowledge of computational complexity, automata theory, basics of logic and proof, and experience with a functional programming language.