See Events

Tangles and Distractions in Parity Games By Tom Van Dijk

Parity games are infinite games between two players on a finite directed coloured graph where the winner of each infinite path is determined by the parity of the highest colour. They are conceptually simple but expressive enough to capture the power of least and greatest fixed points, as evidenced by the tight linear relationship of parity games to the model checking problem of the modal mu-calculus.

We propose that two concepts play a central role for all parity game algorithms, namely a tangle and a distraction. A tangle is the most elementary particle for reasoning why one player cannot avoid playing to certain bad priorities. A distraction is a vertex that literally distracts parity game solvers, slowing progress until the distraction is addressed. Based on this, we propose that a given parity game contains for each player a "distraction tree", as well as "regions of progress". Algorithms that reason on parity games must essentially separate the distraction tree from the region of progress in order to solve parity games.