Supervisor

Suitable for

Abstract

Parity games are a tool for formal verification. For instance, many model checking problems can be reduced to the solution of parity games. The exact complexity of these games is unknown: they can be solved in NP and in coNP, but it is not known whether a polynomial time algorithm exists, despite more than 3 decades of research. However, in practice, most parity games are solved efficiently. This project aims at defining new algorithms for parity games and evaluating them in practice, in particular, over random graphs.

Prerequisites: Discrete Mathematics, Intro. to Formal Proof, Logic and Proof

Desirable: Computer-Aided Formal Verification, Computational Complexity