In this lecture, we consider games played by two players (called 0 and 1), which are zero-sum, perfect information, and most importantly, of potentially infinite duration. Suppose that is a set of -words. Define a game with winning condition  to be:

• a directed graph, not necessarily finite, whose vertices will be called positions of the game;
• a distinguished initial position;
• partition of the positions into positions controlled by player 0  and positions controlled by player 1;
• a labelling function that maps each position to a label from .

The game is played as follows. The game begins in the initial position. The player who controls the initial position chooses an outgoing edge, leading to a new position. The player who controls the new position chooses an outgoing edge, leading to a new position, and so on. If the play reaches a position with no outgoing edges, then the player who controls the position loses immediately. Otherwise, the play continues forever, and yields an infinite path. By applying the labelling function to the path, we get an word in ; if this word belongs to then player 0 wins, otherwise player 1 wins.

When formalizing the notions of the above paragraph, one uses the concept of a strategy. A strategy for player is a function which inputs a history of the play so far (a path from the initial position to some position controlled by player ), and outputs the new position (consistent with the edge relation in the graph). Given strategies for both players, call these and , a unique play is determined, which is either a finite path ending in a terminal position (no outgoing edges), or an infinite path. This play is called winning for player if it is finite and ends in a terminal position controlled by the opposing player ; or if it is infinite and satisfies the winning condition after applying the labelling function. Otherwise, the play is winning for player . A winning strategy for player is defined to be a strategy such that for every possible strategy of the opponent, the resulting play is winning for player .

---

 

Determinacy. A game is called determined if one of the players has a winning strategy. Clearly it cannot be the case that both players have winning strategies. One could be tempted to think that, because of the perfect information, one of the players must have a winning strategy. However, because of the infinite duration, one can come up with strange games (e.g. using the axiom of choice) which are not determined because none of the players has a winning strategy.

The goal of this lecture is to show a theorem by Büchi and Landweber: if the winning condition of the game is recognised by an automaton, then the game is determined, and furthermore the winning player has a finite memory winning strategy, in the following sense.

Finite memory strategy. Consider a game where the positions are . Let be one of the players. A strategy for player with memory  is given by:
• a deterministic automaton with states and input alphabet ; and
• for every position  controlled by , a function from to the neighbors of .
The two ingredients above define a strategy for player in the following way: the next move chosen by player in a position  is obtained by applying the function to the state of the automaton after reading the history of the play, including . We will apply this definition also to games with infinitely many positions, but we will only care about finite memory sets .

An important special case is when the set has only one element, in which case the strategy is called  memoryless. In this case, the new position chosen by the player only depends on the current position, and not on the history of the game before that.

Theorem. (Büchi-Landweber) For every -regular language there exists a finite set such that for every game with winning condition , one of the players has a winning strategy that uses memory .

The proof of the above theorem has two parts. The first part is to identify a special case of games with -regular winning conditions, called parity conditions. Define the -rank parity condition to be the set of -words over the alphabet where the smallest number appearing infinitely often is even. A parity game is a game where the winning condition is the -rank parity language for some .

Parity games are important because not only can they be won using finite memory strategies, but even memoryless strategies are enough:

Theorem 1. For every parity game, one of the players has a memoryless winning strategy.

Theorem 1 is proved here. The second step of the Büchi-Landweber theorem is the reduction to parity games. This essentially boils down to transforming deterministic Muller automata into something called deterministic parity automata. In a parity automaton, there is a ranking function from states to numbers, and a run is considered accepting if the minimal rank appearing infinitely often is even. This is a special case of the Muller condition, but it turns out to be expressively complete in the following sense:

Theorem 2. For every deterministic Muller automaton, there exists an equivalent deterministic parity automaton.

Theorem 2 is proved here. Let us now combine the two theorems to get the Büchi-Landweber theorem. Consider a game with an -regular winning condition . By Theorem 2, there is a deterministic parity automaton which recognises the language . Consider a new game, call it the product game,  where the positions are pairs (position of the original game, state of the deterministic parity automaton). This is a parity game, with the ranks inherited from the automaton. In a position , the player controlling position chooses an edge in the original game, and the state is updated deterministically according to the transition function of the automaton. It is not difficult to see that the following conditions are equivalent for every position of the original game and every player :
1. player wins from position in the original game;
2. player wins from position in the product game, where is the initial state of the automaton.

The implication from 1 to 2 crucially uses determinism of the automaton and would fail if a nondeterministic automaton were used (under an appropriate definition of a product game). Since the product game is a parity game, for every position , condition 2 must hold for either player 0 or 1; furthermore, a positional strategy in the product game corresponds to a finite memory strategy in the original game, where the memory is the states of the automaton.

 

 

COMMENTS