A parity game is an infinite-duration game between two players who pass a token around in a directed graph. The problem of “solving” a parity game (deciding which player wins a given node) is an interesting problem since it is in UP and co-UP, but not known to be in P. In a binary parity game, at least one player can make only binary choices. This allows us to characterise the set of winning strategies (i.e. along which of the two edges this player should move the token) in a propositional formula. In this talk, I will discuss our progress trying to identify the sublogic that corresponds to such characterisations.

This is joint work with Tom Franken and Jan Friso Groote.