In this page, we prove the following theorem:
Theorem (Memoryless Determinacy of Parity Games). In a parity game, one of the players has a memoryless winning strategy.
Recall that in a parity game, the positions are assigned ranks from a set , and the goal of player 0 is to ensure that for infinite plays, the minimal number appearing infinitely often is even. The proof of the theorem is by induction on the number of ranks used in the parity game.
Attractors
Consider a set of positions in a parity game (actually the winning condition is irrelevant for the definition). For a player
, we define below the
-attractor of
, which intuitively represents positions where player
can force a visit to the set
. The attractor is approximated using ordinal numbers – for an ordinal number
, define
to be
plus
• positions owned by player where some outgoing edge leads to
;
• positions owned by the opponent of where all outgoing edges lead to
.
The set grows as
grows, and therefore at some point it stabilises. This stable set is called the
-attractor of
. Over positions in the
-attractor, player
has a memoryless strategy which guarantees that after a finite number of steps, the game will end up in
or in a terminal position owned by the opponent of player
. This strategy, called the attractor strategy, is to go toward
with smaller and smaller index
.
Induction base.
The induction base is when only one rank is used. Let be the parity of the only rank, without loss of generality we assume
. This means that every infinite play is won by player
. This does not necessarily mean that player
wins the game, because the game might end up in a terminal position owned by player
. Let
be the
-attractor of the empty set. We claim that on positions from
, player
has a memoryless winning strategy, and on positions outside
, player
has a memoryless winning strategy. For positions in
, player
plays the attractor strategy, which guarantees reaching a terminal position owned by player
in a finite number of steps. For positions outside
, we make the following observation, which follows immediately from the definition of
:
• if player owns a position outside
, then some outgoing edge leads to a position outside
;
• if player owns a position outside
, then all outgoing edges lead to a position outside
.
It follows that if the play begins outside , then player
has a memoryless strategy that guarantees avoiding
forever, in particular this strategy is winning.
Induction step
The proof is by induction on the number of ranks used
Consider a parity game. For define
to be the set of positions
such that if the initial position is replaced by
, then player
has a memoryless winning strategy. Define
to be the vertices that are in neither
nor in
. Our goal is to prove that
is empty. Here is the picture:
Consider the minimal rank that appears in the entire game, let it be . By symmetry, we assume that this minimal rank is
. (The symmetric case is when the minimal rank is
.) Define
to be the
-attractor, inside the game limited to
, of positions that are in
and have minimal rank
. Here is the picture of the game restricted to
:
In the original game, if the play begins in a position from and player
plays the attractor strategy on the set
, then the play is bound to either end up in a position in
that has rank
, or in the set
. Let us consider the game restricted to set
. Since this game does not use rank
, the induction assumption can be applied to get a partition of
into two sets of positions
and
, such that on each
player
has a memoryless winning strategy, assuming that the game is limited to
:
Here is how the sets can be interpreted in terms of the bigger original game. For every
, if in the original game, if the play begins in a position from
and player
uses the memoryless winning strategy corresponding to
, then either the play stays forever in
and player
wins, or it eventually leaves
.
Here is a picture of the original game with all sets:
Claim. is empty.
Proof. Consider the following memoryless strategy for player in the original game:
• in , use the winning memoryless strategy inherited from the game restricted to
;
• in , use the winning memoryless strategy from the definition of that set;
• on other positions do whatever.
We claim that the above memoryless strategy is winning for all positions from , and therefore
must be empty by assumption on
being all positions where player
can win in a memoryless way. Suppose player
plays the above strategy, and the play begins in
. If the play never leaves
, then player
wins by assumption on the strategy. Suppose that the play does leave
. If it enters
or
, this would have to be a choice of player
, but positions with such a choice already belong to
or
. Therefore, if the play leaves
, then it enters
, where player
wins as well.
In the entire game, consider now the following memoryless strategy for player :
• in , use the winning memoryless strategy inherited from the game restricted to
;
• in , use the winning memoryless strategy from the definition of that set;
• in use the attractor strategy to reach rank
inside
;
• on other positions, i.e. on , do whatever.
We claim that the above strategy wins on all positions except for , and therefore the theorem is proved. We first observe that the play can never enter
, because this would have to be a choice of player
, and such choices are only possible in
. Next we observe that if the play enters
, then player
wins by assumption on
. Other plays will reach positions of rank
infinitely often, by using the attractor, or will stay in
from some point on. In the first case, player
will win by the assumption on
being the minimal rank. In the second case, player
will win by the assumption on
being winning for the game restricted to
.
Leave a Reply