Description

Parity games are a simple concept used to reason about properties of infinite runs of finite systems.

• Does a coffee machine always respond correctly when you ask for coffee?
• Do traffic lights ever enter a forbidden state, causing a collision?
• If a car stops in front of a traffic light, will the light turn green eventually?

You can 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 in the directed graph 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 a play? 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 highest number is an even number, then player Even wins, if it is an odd number, then player Odd wins.

So the 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.

If you are interested in parity games, then there are various BSc topics that you might want to consider. For example: can you prove that certain algorithms are actually correct? Proving properties of algorithms is very important, not just because you want to be absolutely sure that they are correct, but also because you understand more about an algorithm if you can prove certain properties.

• Prove that priority promotion is correct (and gives a correct strategy)
• Prove that tangle learning is correct (and gives a correct strategy)
• Prove that the fixed-point algorithm is correct (and gives a correct strategy)
• Prove that the Two Counters game is an exponential game for tangle learning, priority promotion and/or Zielonka's recursive algorithm (or just one of them)

You can prove such things using tools, like:

• the VerCors tool set
• Isabelle, or Coq (interactive theorem provers)
• Other methods?

See also the list of topics on my website: https://www.tvandijk.nl