Previous chapter: Parity Games
This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner
Muller games differ from the games we have studied so far in that they are not memoryless determined. Consider, for example, a game arena consisting of three positions $v_0,v_1,v_2$, such that there are edges from $v_0$ and $v_2$ to $v_1$ and from $v_1$ to $v_0$ and $v_2$. Hence, the only choice in the game is in $v_1$, where Player 0 gets to choose between moving to $v_0$ or $v_2$:
The Muller condition $\mathcal{F}=\lbrace\lbrace v_0,v_1,v_2\rbrace\rbrace$ is only satisfied if all three positions are visited infinitely often. Player 0 can therefore not win the game with a memoryless strategy, because such a strategy would either visit $v_0$ and $v_1$ infinitely often, or $v_1$ and $v_2$, but not all three positions.
There is, however, a memoryful winning strategy: simply alternate between moving from $v_1$ to $v_0$ and to $v_2$.
In the following, we solve Muller games via a reduction to parity games, i.e., we define a parity game such that we can translate the winning strategy in the parity game into a winning strategy in the Muller game.
The fact that parity games are memoryless determined and Muller games are not, is not a contradiction: our reduction introduces additional state into the parity game, such that, on the extended state space, there exists a memoryless winning strategy. This augmentation of the state space is known as the latest appearence record:
Latest Appearence Record
$\textbf{Definition 11.11. } \text{Let }V\text{ be the set of positions of the game arena and let }{$}\text{ be some fresh}\newline\text{symbol. A }\textit{latest appearence record}\text{ over }V\text{ is a finite word over the alphabet }V\cup\lbrace{$}\rbrace\text{ where every}\newline\text{letter from }V\cup\lbrace{$}\rbrace\text{ appears exactly once and whose first letter is from }V\text{ . The }\textit{hit set}\text{ of a latest}\newline\text{appearence record }\ell=v_0v_1\dots v_m{$}v_m+1\dots v_n\text{ is defined as }hit(\ell)=\lbrace v_0,\dots v_m\rbrace.$
We denote the set of all latest appearence records by $\text{LAR}$. Each latest appearence record represents a permutation of $V$ plus a position indicated by ${$}$.
We will construct the parity game in such a way that whenever the play visits $v_i$, $v_i$ is moved to the beginning of the word, and the ${$}$-symbol is moved to $v_i$’s previous position.
In this way, every play will reach a position such that, from then on, the hit set (i.e., the set of game positions to the left of ${$}$) is always a subset of the infinity set, and infinitely often equal to the infinity set. The winning condition in the parity game thus only needs to ensure that the infinity set is actually one that satisfies the Muller condition.
For this purpose, we assign even colors to hit sets that appear in the table of the Muller condition, and odd colors to hit sets that do not appear in the table. Since the hit set corresponds to subsets of the infinity set, we need to make sure that odd colors that result from strict subsets of entries in the table are ignored.
We do this by increasing the colors depending on the position of the ${$}$-symbol. In this way, the color of the appearence records corresponding to the full infinity set is more important than the colors of the subsets that appear in-between occurrences of the full infinity set.
$\textbf{Definition 11.4. } \text{Let a Muller game }\mathcal{G}=(\mathcal{A},\small\text{MULLER} \normalsize(\mathcal{F}))\text{ with arena }\mathcal{A} = (V,V_0,V_1,E)\newline\text{be given. We compute a parity game }\mathcal{G}’=(\mathcal{A}’,\small\text{PARITY}\normalsize(\mathcal{c}) )\text{ with arena }\mathcal{A}’ = (V’,V_0’,V_1’,E’)\newline\text{ as follows.}$
$\begin{array}{l}
\hspace{0.5cm} \cdot \ V’=V\times\text{LAR},V_0’=V_0\times\text{LAR},V_1’=V_1\times\text{LAR} \newline
\hspace{0.5cm} \cdot \ E’=\lbrace((v,v_0v_1\dots v_m{$}v_{m+1}\dots v_n),(v’,v_0’v_1’\dots v_{j-1}{$}v_{j+1}\dots v_{m+1}\dots v_n))\mid(v,v’)\in E,v’=v_j\rbrace\newline
\hspace{0.5cm} \cdot \ c(v,\ell)= \left\lbrace\begin{array}{ll}
2\cdot |hit(\ell)| & \text{if }hit(\ell)\in\mathcal{F}\newline
2\cdot |hit(\ell)|-1 & \text{if }hit(\ell)\notin\mathcal{F}\newline
\end{array}\right. \newline
\end{array}$
In order to solve a given Muller game, we solve the constructed parity game. To determine if a player has a winning strategy from some position $v$ of the Muller game, we then simply check if the same player wins from the corresponding position of the parity game.
In principle, we could use any position of the parity game where $v$ appears in the first component of the position of the parity game. In the following theorem, we arbitrarily fix the position $(v,v_0v_1\dots v_n{$})$.
$\textbf{Theorem 11.4. } \textit{For every Muller game }\mathcal{G}=(\mathcal{A},\small\text{MULLER} \normalsize(\mathcal{F}))\textit{ with arena }\mathcal{A} = (V,V_0,V_1,E),\newline\textit{there is a parity game }\mathcal{G}’=(\mathcal{A}’,\small\text{PARITY}\normalsize(\mathcal{c}) )\text{ with arena }\mathcal{A}’ = (V’,V_0’,V_1’,E’)\textit{ where}\newline V’=V\times\text{LAR}\textit{ such that each player has a winning strategy from a position }v\in V\textit{ of the Muller}\newline\textit{game iff the same player has a winning strategy from position }(v,v_0v_1\dots v_n{$})\textit{ of the parity game.}$
Please cite the source for reprints, feel free to verify the sources cited in the article, and point out any errors or lack of clarity of expression. You can comment in the comments section below or email to GreenMeeple@yahoo.com