Symbolic solution of Emerson-Lei games

Abstract

Emerson-Lei games have received a lot of focus in recent research. It was only recently that the first symbolic solver algorithm for these games was introduced. As such there has not yet been any implemented game solvers for such games. In this thesis we introduce the first symbolic solver for Emerson-Lei games based on Genie and FairSyn, two game solving tools for Rabin games. We evaluate the performance of our game solver for different types of games, and compare it to FairSyn for Rabin games specifically. Further, as to motivate the practical use of such a solver, we revisit reductions from alternation free μ-calculus to Büchi games and give a reduction formulated using the notation we give for Emerson-Lei games. Based on this reduction we define certificates which we used to argue the correctness of the reduction.