Supervisor

Suitable for

Abstract

Background

The modal mu-calculus is an modal logic used to specify temporal properties of transition systems. Interest in the mu-calculus is partly due to its expressiveness, as many commonly used specification languages such as LTL, CTL, CTL* can be translated into it. The precise complexity of checking whether a formula of the mu-calculus holds true in a transition system is still open, despite considerable efforts.

It is known, however, that the problem is equivalent to computing the winner of a form of combinatorial games called parity games.

Project aims:

The aim of this project is to compare different approaches to computing the winner of parity games according to their performance on various forms of parity games and formulas. As part of the project, an algorithm based on a reduction to SAT and a deterministic sub-exponential time algorithm for solving parity games need to be implemented.

Prerequisites:

The candidate should have experience in programming in languages such as C/C++ and Java and a general interest in areas of theoretical computer science such as automata theory, logic, verification, or combinatorics.

While a course on Logic, Automata, and Games is not a strict requirement, it would certainly be helpful.