Guest Talk: Tom van Dijk: Tangles and Distractions in Parity Games

Tuesday, October 01, 2019, 10:30am

Location: RWTH Aachen University, Department of Computer Science - Ahornstr. 55, building E3, room 9u10

Speaker: Tom van Dijk

 

Abstract:

Parity games are infinite games between two players on a finite directed colored graph where the winner of each infinite path is determined by the parity of the highest color. 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 a 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.