|title:||Parity games and Groove|
|keywords:||parity games, groove, visualisation|
Tom van Dijk
Parity games are a simple model used to reason about properties of infinite runs of finite systems. For example, does a coffee machine always respond when you ask for coffee? Do traffic lights never enter a forbidden state? You can not only use parity games to prove whether a system has a property, but also to automatically construct a system with a given property, this is called "controller synthesis".
A parity game is played on a finite directed graph between two players, player Even and player Odd. Typically these are the controller vs the environment, or the prover vs the disprover. Each vertex has at least one successor and each vertex is owned by exactly one of the players. The owner of the vertex decides which successor vertex to take. This way the two players play an infinite game. Now how do we decide the winner of the game? The vertices are assigned natural numbers (0, 1, 2...) and we look at the numbers that we see infinitely often in the play, that is, because the graph is finite, all plays in the game contain cycles, so we look at the numbers on these cycles. The highest number that is seen infinitely often determines the winner. If this is an even number, then player Even wins, if this is an odd number, then player Odd wins.
So the whole goal for player Even is to always select a successor such that no matter what player Odd does, the highest number on every cycle that Odd can play to is even. And vice versa for player Odd.
It is known from the literature that every vertex is won by one of the players (meaning that you have a winning region of Even and a winning region of Odd in the game) and that in the regions that they win, the players have a strategy for the vertices that they control, which selects one successor. Then no matter how the opponent plays, all cycles in the winning region are won by the winner as long as the winner plays according to this strategy.
Many algorithms have been invented to solve parity games, in part because parity games are a simple example of a problem that we as researchers believe should be solvable in Polynomial Time, but we do not yet know how.
This BSc Research Project is about implementing parity game algorithms in Groove. Groove offers a very nice user interface for manipulating graphs. It would be nice to be able to use Groove to solve a parity game using any algorithm that you like. Suggested algorithms are priority promotion, Zielonka's recursive algorithm, tangle learning.