Symbolic solution of Emerson-Lei games
Ladda ner
Typ
Examensarbete för masterexamen
Master's Thesis
Master's Thesis
Program
Computer science – algorithms, languages and logic (MPALG), MSc
Publicerad
2024
Författare
Larsson, Christopher
Jakobson Mo, Nils
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
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.
Beskrivning
Ämne/nyckelord
Computer science , Algorithms , Logic , Emerson-Lei , Thesis , Games , Game solving , Reduction , Certificates