An Arithmetic Approach to Parity Games
Project by Dr. Sebastian Mueller between March 2014 and December 2015.
Description
Parity Games are 2-player games played on finite directed graphs with integer vertex labels. Both players take terms moving a token along the graph for an infinite number of times and the winner is decided by the parity of the highest valued label that appears an infinite number of times in the play. Being a subclass of Borel Games, Parity Games are determined. That is, one of the players can win the game, no matter how his adversary plays.
Moreover, it is quite easy to see that determining the Player who has a winning strategy is in NP as well as in co-NP. The obvious open question, whether Parity Games is also in P has not been answered, albeit being heavily investigated. An important equivalent problem is the model checking problem for the modal μ-calculus, which makes these games even more interesting for a logician.
In this project, we aim at formalising the proof of determinacy in a weak arithmetic theory and, using that formalisation, hope to be able to show that Parity Games lies somewhere low in the Parameterized Hierarchy, at best, that it is fixed parameter tractable. To do so, we develop new arithmetic theories that reflect these computational classes and investigate parameterizations of the underlying graphs that help in simplifying the original argument.
