Last time, we described how parity games could be seen as an algorithmic backend to verification problems in practice. In this post of the series, we introduce parity games concretely and explain why they are an interesting subject on their own from a complexity theoretic (we’ll get to that) point of view.
From a game-theoretic point of view, a parity game is a two-player zero-sum perfect-information game. Let’s decode what that means. First, two-player game means that there are two players playing this game, like in chess.
Now zero-sum means that for one player to be winning the other player must be losing. Many casual games are zero-sum games. In more general terms, zero-sum means the following: after the two players have played the game, they both get an outcome of the play – that could, for instance, be money that a player gets or that a player has to pay. Whatever amount one player gains must be at loss for the other player. In other words the sum of the outcomes for both players must be zero. In our scenario we could say that winning results in outcome 1 while losing results in outcome -1, hence the sum will always be zero.
Third, it’s a perfect-information game. That means that both players know the complete state of the game at any time. Chess, for instance, is a perfect-information game, because both players can see the whole board. Most card games, on the other hand, are imperfect-information games, because the players can’t see which cards the other players have. They can guess, of course, and compute probabilities, but in general they don’t know for sure which cards the other people hold.
So how do parity games look like? First of all mind the plural: parity games really describe a class of games – there are infinitely many different parity games. To put that into perspective, the contemporarily popular Sudoku games are also a class of games – there many different instances of the Soduko grid to start with.
Parity games are so-called graph-based games. A graph consists of two ingredients: a set of positions, called nodes, and a set of (one-way) connections, called edges. Every edge in a graph connects two nodes with each other. For our purposes, a graph can be seen as the abstraction of a game board – they usually look grid-like and every position is directly connected to its immediate neighbors. But parity games don’t necessarily connect immediate neighbors with each other. Additionally, we want to have “bridges” that connect nodes being far away with each other. So a graph really is an abstraction of the two-dimensional game boards.
The nodes (positions) of the graph have two shapes: circular and rectangular. The circular nodes belong to player 0, the rectangular nodes belong to player 1. For mathematical reasons, we call both players 0 and 1 instead of 1 and 2. We also call them player “Even” and player “Odd”. Furthermore, every node is labeled with a natural number. Intuitively, player Even likes large even numbers and player Odd likes large odd numbers. The game is played by putting a pebble on a designated starting node of the graph. If this starting node belongs to Even, then she can choose one of the outgoing edges (connections) and moves the token along the chosen edge to a new node. Otherwise, it’s Odd’s turn to choose the edge. The game then continues in that fashion for an infinite number of steps.
Wait a minute – how could two players play for an infinite number of steps? Of course, this could not be done by real living players. We will see later how this strange issue can be resolved. But bear with me for the time being. Just assume that both players played for an infinite number of steps – resulting, for instance, in the following sequence of nodes:
4, 1, 6, 8, 2, 0, 3, 2, 0, 3, 2, 0, 3, 2, 0, 3, …
Who wins this play? The winning condition is as follows: if the largest number that occurs infinitely often is even, Even wins; otherwise, Odd wins. So in this example play, player Odd wins, because 3 is the largest number (called priority) that occurs infinitely often.
The algorithmic question is, given a parity game and a designated starting position, can we tell whether one of the two players has a winning strategy against the other player? In other words, is there a clever plan for one of the two players such that no matter what the opponent does, the player is winning? And if so, can we also understand why?
The answer to all these questions is yes: parity games are determined, so there must be a winning strategy for one of the players from a designated starting position; we can also algorithmically decide which of the two players can win; furthermore, we can provide an additional winning strategy that witnesses the clear win of the respective player.
If you think about it, it follows that the witnessing winning strategy must have a finite description, otherwise there could be no way for the algorithm to print it out. So how could strategies possibly look like for both players?
A strategy should tell the player which outgoing edge to take from a node when the pebble has been put on it. This decision can depend on the whole history of the play, i.e. on everything that has happened beforehand. So in general, a strategy can be an object of infinite size. Luckily, parity games are not only determined, but positionally determined. That means that there is no strategic benefit in making decisions depend on the history. If a player chooses to move from node v to node u at some point, then the player should stick to that choice – in other words whenever the pebble falls back to node v, the player should choose the edge leading to node u again. Such positional strategies are finite objects. So why is there no strategic benefit in non-positional strategies? We will see that whenever we have found a non-positional winning strategy, we can also find a positional winning strategy – so there is no need to hassle around with non-positional strategies in the first place.
Consider the example parity game again for a minute. The blue respectively red areas describe the winning sets of both player Even and player Odd. A winning set is the set of node from which the respective player has a winning strategy. The boldly marked blue and red edges are witnessing positional winning strategies. You can try it out yourself: no matter which choices you make as an opponent (being it positional or non-positional choices), you will lose against the other player in his / her winning region.
Which brings us back to the algorithmic question: deciding which player has a positional winning strategy from a designated starting node. As we will also see, it is easy to determine whether a given positional strategy is indeed a winning strategy. So algorithmically, this problems is in the complexity class NP – but we don’t know whether it is NP-hard nor do we know whether is in P. Because of the positional determinacy, the problem is also contained in coNP. In case you have no idea what I’m talking about, please read the wonderful article by Scott Aaronson on the NP/P-problem which is one of the most important open problems in maths and theoretical computer science. Since there are not many natural problems that are contained in both NP and coNP without being easily seen to be in P, the problem of parity game solving touches one of the most interesting subjects of pure complexity theory. In other words, it would be a major break-through if we could prove parity game solving to be in P. Or if we could prove it’s NP-hard which (I guess) no one really believes.
The next post in this series will feature an algorithm that solves parity games and prove some interesting results along the way.