# The backward approach of Muller and Schupp for positional determinacy

This post revisits Muller and Schupp's backward approach to prove the positionality of parity games. The argument is simple and beautiful; credits go to Thomas Colcombet for this presentation.

We discussed the technical details of the construction informally together, and Thomas gave me a draft he wrote. Unhappy that I didn't write the draft myself, I wrote down my own version of the construction. It turned out to be technically identical. This post features additional explanations and unhelpful drawings.

The crux in a few sentences: assume we have a winning strategy for parity, we want to construct a positional one. The difficulty is that the strategy we start from may perform stupid moves at various times during the game. We define a preference order on plays, which induces the notion of the worst possible history when reaching a vertex. The positional strategy plays assuming this worst case; if the preference order is well chosen, this forces the strategy to play good moves, ensuring the parity condition.

We fix $\G$ a game with finite outdegree, $v_0$ a starting vertex and $\sigma$ a winning strategy for Eve, i.e. ensuring $\Parity$.

#### Ordering histories

A history is a finite or infinite word over $\priority$, we let be the set of histories. It is equipped with the prefix distance, inducing a notion of limit for sequences of histories.

The parity condition is satisfied by infinite histories such that the *maximal* priority appearing infinitely
often is even.

For a history $p$, define $\tr_c(p)$ the suffix of $p$ that starts after the last occurrence of $c$. The infix from position $n$ to position $m$ is written $p[n,\ldots,m]$. For a history $p$, define $\xi_c(p)$ the set of positions for which $p$ has value $c$.

We will consider sets of natural numbers, ordered by $\lex$ defined as follows: for two sets $X,Y \subseteq \N$, we say that $X \lexstrict Y$ if there exists $n \in \N$ such that $n \in Y \setminus X$ and $X \cap \set{0,\ldots,n-1} = Y \cap \set{0,\ldots,n-1}$.

We define the order $\preceq$ over for finite histories; intuitively speaking, $p \preceq q$ reads: $p$ is worse than $q$ with respect to $\Parity$. We first define $\preceq_d$ by induction on the maximal priority $d$:

- If $d = 0$, then $p \preceq_d\ q$ if $|p| \le |q|$.
- If $d$ is odd, then $p \preceq_d\ q$ if
- If $d$ is even and different from $0$, then $p \preceq_d\ q$ if

Now define $\preceq$ as $\preceq_d$.

Fact:If $p \preceq q$, then for all $r$ we have $p \cdot r \preceq q \cdot r$.

#### Defining a positional strategy for Eve

A play is a finite or infinite word over $V$, which naturally induces a history. We assume that plays start in $v_0$. We identify a play and its induced history: for instance, for $\pi_1,\pi_2$ two finite plays, we say that $\pi_1 \preceq \pi_2$ if $c(\pi_1) \preceq c(\pi_2)$ holds, where $c(\pi_1)$ and $c(\pi_2)$ are the histories induced by $\pi_1$ and $\pi_2$.

In the following lemma, we make use of the finite-degree assumption.

Lemma:Let $(p_n)\nN$ be a sequence of finite plays. Then it contains a converging subsequence.

We define a positional strategy $\sigma’$ on all vertices reachable by $\sigma$. The definition is by induction on the rank, which is the length of the smallest path from $v_0$. For the definition to make sense we need to ensure the following property: for all vertices $v$ reachable by $\sigma’$, there exists a play ending in $v$ consistent with both $\sigma$ and $\sigma’$.

Assume that $\sigma’$ has been defined on all vertices of rank $k$, then for all vertices $v \in \VE$ of rank $k+1$ reachable by $\sigma’$, define $\sigma’(v) = \sigma(\pi_v)$, where $\pi_v$ is a finite play ending in $v$ and consistent with both $\sigma$ and $\sigma’$, minimal with respect to $\preceq$ among all such plays. The property is clearly preserved by this construction.

Theorem:The strategy $\sigma’$ ensures $\Parity$.

**Proof:**
Consider a play $\pi = v_0 v_1 \ldots$ consistent with $\sigma’$.

For the sake of readability, write $\pi_n = \pi_{v_n}$. We first observe that $\pi_{n+1} \preceq \pi_n \cdot v_{n+1}$ for all $n$. Indeed, by definition of $\sigma’$, the play $\pi_n \cdot v_{n+1}$ is consistent with both $\sigma$ and $\sigma’$. Since the play $\pi_{n+1}$ is the worst play ending in $v_{n+1}$ consistent with both $\sigma$ and $\sigma’$, it is smaller than $\pi_n \cdot v_{n+1}$ with respect to $\preceq$.

Using this inequality, an easy induction shows that $\pi_m \preceq \pi_n \cdot \pi[n+1,\ldots,m]$ for all $n < m$, and also $\pi_n \preceq \pi[0,\ldots,n]$. Here we rely on the fact above.

Thanks to the lemma above, the sequence $(\pi_n)\nN$ contains a subsequence indexed by $I \subseteq \N$ which converges to an infinite play, written $\pi_\infty$. Observe that since for all $n \in I$, the finite play $\pi_n$ is consistent with $\sigma$, the limit $\pi_\infty$ is consistent with $\sigma$ hence satisfies $\Parity$.

We conclude using the following lemma.

Lemma:Let $\pi = v_0 v_1 \ldots$ be an infinite play and $(\pi_n)\nN$ be a sequence of finite plays, such that:

- $(\pi_n)\nN$ converges to an infinite play $\pi_\infty$,
- $\pi_\infty$ satisfies $\Parity$,
- for all $n$, $\pi_{n+1} \preceq \pi_n \cdot \pi[|\pi_n+1|,\ldots,|\pi_{n+1}|]$.

Then $\pi$ satisfies $\Parity$.

**Proof:**
We proceed by induction on the maximal priority $d$.
The case $d = 0$ is easy.

*First case:* $d$ is even and different from $0$.
There are two cases:

- Either $d$ appears infinitely many times in $\pi_\infty$. We show the following property:

For every $k$ such that $c(\pi_\infty)(k) = d$, there exists $k’ \ge k$ such that $c(\pi)(k’) = d$.

Consider such a $k$ and $\pi_n$ that coincides with $\pi_\infty$ on the first $k$ positions. Since $\pi_n \preceq \pi[0,\ldots,n]$, by definition $\max(\xi_d(\pi_n)) \le \max(\xi_d(\pi[0,\ldots,n]))$. Observe that $\max(\xi_d(\pi_n)) \ge k$ since $k \in \xi_d(\pi_n)$, so $\max(\xi_d(\pi[0,\ldots,n])) \ge k$, and the conclusion follows.

It follows that $d$ appears infinitely many times in $\pi$, so $\pi$ satisfies $\Parity$.

- Or $d$ appears finitely many times in $\pi_\infty$. We conclude by induction hypothesis, considering the sequence $(\tr_d(\pi_n))\nN$.

*Second case:* $d$ is odd.
We show the following property:

For every $n$, for every $k \ge n$ such that $c(\pi(k)) = d$, there exists $k’ \ge n$ such that $c(\pi_\infty(k’)) = d$.

Consider such $k$ and $k$ and $n_0,n_1$ such that $\pi_{n_0}$ coincides with $\pi_\infty$ on the first $n$ positions, and $\pi_{n_1}$ coincides with $\pi_\infty$ on the first $k$ positions. Without loss of generality, $n < n_0 < k < n_1$. We have $\pi_{n_1} \preceq \pi_{n_0} \cdot \pi[n_0+1,\ldots,n_1]$, so

Since $c(\pi(k)) = d$, there exists $k’ \le k$ such that $c(\pi_{n_1}(k’)) = d$. Since $\pi_{n_0}$ and $\pi_{n_1}$ both coincide with $\pi_\infty$ on the first $n$ positions, there are equal up to this position, so $k’ > n$. Since $\pi_{n_1}$ coincide with $\pi_\infty$ on the first $k$ positions, it follows that $c(\pi_\infty(k’)) = d$.

Since $d$ appears finitely many times in $\pi_\infty$, it implies that $d$ appears finitely many times in $\pi$. As above, we conclude by induction hypothesis, considering the sequence $(\tr_d(\pi_n))\nN$.