Games automata play

Positional determinacy for parity games, a forward approach

August 02, 2018 | by Nathanaël Fijalkow

This post gives a proof of positional determinacy for parity games. One may recognise it in the works of Emerson and Jutla (91) using modal mu-calculus, and also more explicitely in the works of Kupferman and Vardi (98).

We fix some notations. Consider a finite parity game with $n$ vertices and priorities in $[1,d]$. The parity condition is satisfied by a play if the maximal priority seen infinitely often is even, we write $\Parity_d$ to mean that the priorities range in $[1,d]$. The two players are Eve and Adam, she controls the vertices depicted by circles and he controls the vertices depicted by squares. We let $W_E(\Parity_d)$ denote the set of vertices from which Eve has a winning strategy, and $W_A(\Parity_d)$ for Adam.

For a set of vertices $U \subseteq V$, we let $\Pre(U) \subseteq V$ be the set of vertices from which Eve can ensure to reach $U$ in one step: We use $\overline{\Pre(U)}$ for the complement of $\Pre(U)$. The condition $\Reach(U)$ is satisfied by plays visiting $U$ at least once, and $\Safe(U)$ by plays never visiting $U$. We write $V_d$ for the set of vertices of priority $d$.

Two recursive lemmas

The inductive statement is as follows: we consider parity games with priorities in $[1,d]$ and two additional colours: $\Win$ and $\Lose$. The vertices with colours $\Win$ or $\Lose$ are terminal: when reaching a terminal vertex, the game stops and one of the players is declared the winner. Formally, the objective is

Lemma: Assume that $d$ is even. is the greatest fixed point of the operator $Y \mapsto$

For the sake of the explanation and in the proof, we assume that $\Win = \Lose = \emptyset$.

In words: $W_E(\Parity_d)$ is the largest set of vertices $Y$ such that from $Y$ Eve has a strategy ensuring that

  • either the priority $d$ is never seen, in which case the parity condition is satisfied with lower priorities,
  • or the priority $d$ is seen, in which case Eve can ensure to reach $Y$ in one step.
The even case.

Proof: The fact that $W_E(\Parity_d)$ contains the greatest fixed point follows from the observation that any fixed point $Y$ is contained in $W_E(\Parity_d)$. Indeed, if $Y$ is a fixed point, the strategy described above ensures parity: either it visits finitely many times $d$, and then from some point onwards the parity condition is satisfied with lower priorities, or it visits infinitely many times $d$, and then the parity condition is satisfied because $d$ is maximal and even.

Note that we are constructing positional strategies by taking the disjoint union of two positional strategies, one for $W_E(\Parity_{d-1})$ for vertices of priorities less than $d$ and the other for $d \cap \Pre(W_E(\Parity_{d-1}))$.

The fact that $W_E(\Parity_d)$ is included in the greatest fixed point follows from the fact that it is itself a fixed point, which is easy to check.

Lemma: Assume that $d$ is odd. Then $W_E (\left( \Parity_d \cup \Reach(\Win) \right) \cap \Safe(\Lose) )$ is the least fixed point of the operator $X \mapsto$

For the sake of the explanation and in the proof, we assume that $\Win = \Lose = \emptyset$.

In words: $W_E(\Parity_d)$ is the smallest set of vertices $X$ such that from $X$ Eve has a strategy ensuring that

  • either the priority $d$ is never seen, in which case the parity condition is satisfied with lower priorities,
  • or the priority $d$ is seen, in which case Eve can ensure to reach $X$ in one step.
The odd case.

Proof: The fact that $W_E(\Parity_d)$ contains the least fixed point follows from the fact that it is itself a fixed point, which is easy to check.

The fact that $W_E(\Parity_d)$ is included in the least fixed point is the interesting non-trivial bit. It follows from the observation that any fixed point $X$ contains $W_E(\Parity_d)$. To prove this, we show that $V \setminus X \subseteq W_A(\Parity_d) \subseteq V \setminus W_E(\Parity_d)$. Note that here we are not relying on the determinacy of parity games: the second inclusion is very simple and always true, it only says that Eve and Adam cannot win from the same vertex.

Indeed, if $X$ is a fixed point, from $V \setminus X$ Adam has a strategy ensuring that

  • either the priority $d$ is never seen, in which case the parity condition is violated with lower priorities,
  • or the priority $d$ is seen, in which case Adam can ensure to reach $V \setminus X$ in one step.

This strategy violates parity: either it visits finitely many times $d$, and then from some point onwards the parity condition is violated with lower priorities, or it visites infinitely many times $d$, and then the parity condition is violated because $d$ is maximal and odd.

Remark: We could have said that the odd case is symmetric to the even case, swapping the role of the two players. Indeed, the two claims are in some sense dual to each other (more precisely, this amount to negate the modal mu-calculus formula). We do not take this road, because it requires assuming determinacy of parity games, which we avoided in this presentation, and obtained as a corollary.

Finishing the proof

We now explain how the two lemmas show that if parity games with priorities in $[1,d-1]$ are positionally determined, then parity games with priorities in $[1,d]$ are positionally determined. Let

Depending on the parity of $d$, either of the two lemmas show that

with $\Win’ = \Win \cup (V_d \cap \Pre(W))$ and $\Lose’ = \Lose \cup (V_d \cap \overline{\Pre(W)})$

Observe that the latter can be seen as a parity game with priorities in $[1,d-1]$, because vertices with priority $d$ have been added either to $\Win’$ or to $\Lose’$. Let $\sigma_{d-1}$ be a positional winning strategy in this game. The proof yields a positional winning strategy in the original game by taking the disjoint union of $\sigma_{d-1}$ and of the (positional) strategy $\sigma_d$ ensuring from $V_d \cap \Pre(W)$ to reach $W$ in one step. This concludes the proof.