Gastvortrag: Tom van Dijk: Tangles and Distractions in Parity Games

Dienstag, 01.10.2019, 10.30 Uhr

Ort: RWTH Aachen University, Informatikzentrum - Ahornstr. 55, Erweiterungsgebäude E3, Raum 9u10

Vortragender: 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.