Solving Parity Games in Practice (to replace Parity Games over Random Graphs)
AbstractParity 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. Recently, a quasi-polynomial algorithm for parity games was developed, which reinforces the believe that parity games may be efficiently solved in practice. The goal of this project is to produce an implementation of the new algorithm and to evaluate its performance in practice, in particular, with respect to the set of algorithms already implemented, for instance, those that can be solved using PGSolver. The study should be conducted using a set of benchmarks as well as on random graphs.
Prerequisites: Discrete Mathematics; Computer-Aided Formal Verification, Computational Complexity
Desirable: Automata, Logic and Games; Computational Game Theory Project type: Practice