Symmetric Strategy Improvement

Introduction

We study turn-based graph games between two players—Player Min and Player Max—who take turns to move a token along the vertices of a coloured finite graph so as to optimise their adversarial objectives. Various classes of graph games are characterised by the objective of the players, for instance in parity games the objective is to optimise the parity of the dominating colour occurring infinitely often, while in discounted and mean-payoff games the objective is the discounted and limit-average sum of the colours. Solving graph games is the central and most expensive step in many model checking , satisfiability checking , and synthesis algorithms. More efficient algorithms for solving graph games will therefore foster the development of performant model checkers and contribute to bringing synthesis techniques to practice.

Parity games enjoy a special status among graph games and the quest for performant algorithms for solving them has therefore been an active field of research during the last decades. Traditional forward techniques ($\approx O(n^{\frac{1}{2}c})$ for parity games with $n$ positions and $c$ colours), backward techniques ($\approx O(n^{c})$ ), and their combination ($\approx O(n^{\frac{1}{3}c})$ ) provide good complexity bounds. However, these bounds are sharp, and techniques with good complexity bounds frequently display their worst case complexity on practical examples. Strategy improvement algorithms , on the other hand, are closely related to the Simplex algorithm for solving linear programming problems that perform well in practice.

Classic strategy improvement algorithms are built around the existence of optimal positional strategies for both players. They start with an arbitrary positional strategy for a player and iteratively compute a better positional strategy in every step until the strategy cannot be further improved. Since there are only finitely many positional strategies in a finite graph, termination is guaranteed. The crucial step in a strategy improvement algorithm is to compute a better strategy from the current strategy. Given a current strategy $\sigma$ of a player (say, Player Max), this step is performed by first computing the globally optimal counter strategy $\tau^{c}_{\sigma}$ of the opponent (Player Min) and then computing the value of each vertex of the game restricted to the strategies $\sigma$ and $\tau^{c}_{\sigma}$. For the games under discussion (parity, discounted, and mean-payoff) both of these computations are simple and tractable. This value dictates potentially locally profitable changes or switches $\mathsf{Prof}(\sigma)$ that Player Max can make vis-à-vis his previous strategy $\sigma$. For the correctness of the strategy improvement algorithm it is required that such locally profitable changes imply a global improvement. The strategy of Player Max can then be updated according to a switching rule (akin to pivoting rule of the Simplex) in order to give an improved strategy. This has led to the following template for classic strategy improvement algorithms.

A number of switching rules, including the ones inspired by Simplex pivoting rules, have been suggested for strategy improvement algorithms. The most widespread ones are to select changes for all game states where this is possible, choosing a combination of those with an optimal update guarantee, or to choose uniformly at random. For some classes of games, it is also possible to select an optimal combination of updates . There have also been suggestions to use more advanced randomisation techniques with sub-exponential – $2^{O(\sqrt{n})}$ – bounds and snare memory . Unfortunately, all of these techniques have been shown to be exponential in the size of the game .

Classic strategy improvement algorithms treat the two players involved quite differently where at each iteration one player computes a globally optimal counter strategy, while the other player performs local updates. In contrast, a symmetric strategy improvement algorithm symmetrically improves the strategies of both players at the same time, and uses the finding to guide the strategy improvement. This suggests the following naïve symmetric approach.

This algorithm has earlier been suggested by Condon where it was shown that a repeated application of this update can lead to cycles . A problem with this naïve approach is that there is no guarantee that the primed strategies are generally better than the unprimed ones. With hindsight this is maybe not very surprising, as in particular no improvement in the evaluation of running the game with $\sigma^{\prime},\tau^{\prime}$ can be expected over running the game with $\sigma,\tau$, as an improvement for one player is on the expense of the other. This observation led to the approach being abandoned. In this paper we propose the following more careful symmetric strategy improvement algorithm that guarantees improvements in each iteration similar to classic strategy improvement.

The main difference to classic strategy improvement approaches is that we exploit the strategy of the other player to inform the search for a good improvement step. In this algorithm we select only such updates to the two strategies that agree with the optimal counter strategy to the respective other’s strategy. We believe that this will provide a gradually improving advice function that will lead to few iterations. We support this assumption by showing that this algorithm suffices to escape the traps Friedmann has laid to establish lower bounds for different types of strategy improvement algorithms .

Preliminaries

We focus on turn-based zero-sum games played between two players—Player Max and Player Min—over finite graphs. A game arena $\mathcal{A}$ is a tuple $(V_{\textrm{Max}},V_{\textrm{Min}},E,C,\phi)$ where $(V=V_{\textrm{Max}}\cup V_{\textrm{Min}},E)$ is a finite directed graph with the set of vertices $V$ partitioned into a set $V_{\textrm{Max}}$ of vertices controlled by Player Max and a set $V_{\textrm{Min}}$ of vertices controlled by Player Min, $E\subseteq V\times V$ is the set of edges, $C$ is a set of colours, $\phi:V\to C$ is the colour mapping. We require that every vertex has at least one outgoing edge.

In the remainder of this paper, we will use parity games where every colour is unique, i.e., where $\phi$ is injective. All parity games can be translated into such games as discussed in . For these games, we use a valuation function based on their progress measure. We define $\eta$ as $\langle c_{0},c_{1},\ldots\rangle\mapsto(c,C,d)$, where $c=\limsup_{i\rightarrow\infty}c_{i}$ is the dominant colour of the colour sequence, $d=\min\{i\in\omega\mid c_{i}=c\}$ is the index of the first occurrence of $c$, and $C=\{c_{i}\mid i<d,c_{i}>c\}$ is the set of colours that occur before the first occurrence of $c$. The preference order is defined as the following: we have $(c^{\prime},C^{\prime},d^{\prime})\prec(c,C,d)$ if

$c{=}c^{\prime}$, the highest colour $h$ in the symmetric difference between $C$ and $C^{\prime}$ is even, and in $C$,

$c{=}c^{\prime}$, the highest colour $h$ in the symmetric difference between $C$ and $C^{\prime}$ is odd, and in $C^{\prime}$,

$c=c^{\prime}$ is even, $C=C^{\prime}$, and $d<d^{\prime}$, or

$c=c^{\prime}$ is odd, $C=C^{\prime}$, and $d>d^{\prime}$.

A strategy of Player Max is a function $\sigma:V^{*}V_{\textrm{Max}}\rightarrow V$ such that \big{(}v,\sigma(\pi v)\big{)}\in E for all $\pi\in V^{*}$ and $v\in V_{\textrm{Max}}$. Similarly, a strategy of Player Min is a function $\tau:V^{*}V_{\textrm{Min}}\rightarrow V$ such that \big{(}v,\sigma(\pi v)\big{)}\in E for all $\pi\in V^{*}$ and $v\in V_{\textrm{Min}}$. We write $\Sigma^{\infty}$ and $T^{\infty}$ for the set of strategies of Player Max and Player Min, respectively.

For a strategy pair $(\sigma,\tau)\in\Sigma^{\infty}\times T^{\infty}$ and an initial vertex $v\in V$ we denote the unique play starting from the vertex $v$ by $\pi(v,\sigma,\tau)$ and we write $\mathsf{val}_{\mathcal{G}}(v,\sigma,\tau)$ for the value of the vertex $v$ under the strategy pair $(\sigma,\tau)$ defined as

We also define the concept of the value of a strategy $\sigma\in\Sigma^{\infty}$ and $\tau\in T^{\infty}$ as

We also extend the valuation for vertices to a valuation for the whole game by defining $V$ dimensional vectors $\mathsf{val}_{\mathcal{G}}(\sigma):v\mapsto\mathsf{val}_{\mathcal{G}}(v,\sigma)$ with the usual $V$ dimensional partial order $\sqsubseteq$, where $\mathsf{val}\sqsubseteq\mathsf{val}^{\prime}$ if, and only if, $\mathsf{val}(v)\preceq\mathsf{val}^{\prime}(v)$ holds for all $v\in V$.

We say that a strategy $\sigma\in\Sigma^{\infty}$ is memoryless or positional if it only depends on the last state, i.e. for all $\pi,\pi^{\prime}\in V^{*}$ and $v\in V_{\textrm{Max}}$ we have that $\sigma(\pi v)=\sigma(\pi^{\prime}v)$. Thus, a positional strategy can be viewed as a function $\sigma:V_{\textrm{Max}}\to V$ such that for all $v\in V_{\textrm{Max}}$ we have that $(v,\sigma(v))\in E$. The concept of positional strategies of Player Min is defined in an analogous manner. We write $\Sigma$ and $T$ for the set of positional strategies of Players Max and Min, respectively. We say that a game is positionally determined if:

$\mathsf{val}_{\mathcal{G}}(v,\sigma)=\min_{\tau\in T}\mathsf{val}_{\mathcal{G}}(v,\sigma,\tau)$ holds for all $\sigma\in\Sigma$,

$\mathsf{val}_{\mathcal{G}}(v,\tau)=\max_{\sigma\in\Sigma}\mathsf{val}_{\mathcal{G}}(v,\sigma,\tau)$ holds for all $\tau\in T$,

Existence of value: for all $v\in V$ $\max_{\sigma\in\Sigma}\mathsf{val}_{\mathcal{G}}(v,\sigma)=\min_{\tau\in T}\mathsf{val}_{\mathcal{G}}(v,\tau)$ holds, and we use $\mathsf{val}_{\mathcal{G}}(v)$ to denote this value, and

Existence of positional optimal strategies: there is a pair $\tau_{\min},\sigma_{\max}$ of strategies such that, for all $v\in V$, $\mathsf{val}_{\mathcal{G}}(v)=\mathsf{val}_{\mathcal{G}}(v,\sigma_{\max})=\mathsf{val}_{\mathcal{G}}(v,\tau_{\min})$ holds. Observe that for all $\sigma\in\Sigma$ and $\tau\in T$ we have that $\mathsf{val}_{\mathcal{G}}(\sigma_{\max})\sqsupseteq\mathsf{val}_{\mathcal{G}}(\sigma)$ and $\mathsf{val}_{\mathcal{G}}(\tau_{\min})\sqsubseteq\mathsf{val}_{\mathcal{G}}(\tau)$.

Observe that (first and second item above) that classes of games with positional strategies guarantee an optimal positional counter strategy for Player Min to all strategies $\sigma\in\Sigma$ of Player Max. We denote these strategies by $\tau^{c}_{\sigma}$. Similarly, we denote the optimal positional counter strategy for Player Max to a strategy $\tau\in T$ by $\sigma^{c}_{\tau}$ of Player Min. While this counter strategy is not necessarily unique, we use the convention in all proofs that $\tau^{c}_{\sigma}$ is always the same counter strategy for $\sigma\in\Sigma$, and $\sigma^{c}_{\tau}$ is always the same counter strategy for $\tau\in T$.

Consider the parity game arena shown in Figure 1. We use circles for the vertices of Player Max and squares for Player Min. We label each vertex with its colour. Notice that a positional strategy can be depicted just by specifying an outgoing edge for all the vertices of a player. The positional strategies $\sigma$ of Player Max is depicted in blue and the positional strategy $\tau$ of Player Min is depicted in red. In the example, $\mathsf{val}(1,\sigma,\tau)=(1,\emptyset,0)$, $\mathsf{val}(4,\sigma,\tau)=(3,\{4\},1)$, $\mathsf{val}(3,\sigma,\tau)=(3,\emptyset,0)$, and $\mathsf{val}(0,\sigma,\tau)=(0,\emptyset,0)$.

As discussed in the introduction, classic strategy improvement algorithms work well for classes of games that are positionally determined. Moreover, the evaluation function should be such that one can easily identify the set $\mathsf{Prof}(\sigma)$ of profitable updates and reach an optimum exactly where there are no profitable updates. We formalise these prerequisites for a class of games to be good for strategy improvement algorithm in this section.

For a strategy $\sigma\in\Sigma$, an edge $(v,v^{\prime})\in E$ with $v\in V_{\textrm{Max}}$ is a profitable update if $\sigma^{\prime}\in\Sigma$ with $\sigma^{\prime}:v\mapsto v^{\prime}$ and $\sigma^{\prime}:v^{\prime\prime}\mapsto\sigma(v^{\prime\prime})$ for all $v^{\prime\prime}\neq v$ has a strictly greater evaluation than $\sigma$, $\mathsf{val}_{\mathcal{G}}(\sigma^{\prime})\sqsupset\mathsf{val}_{\mathcal{G}}(\sigma)$. We write $\mathsf{Prof}(\sigma)$ for the set of profitable updates.

In our example from Figure 1, $\tau=\tau_{\sigma}^{c}$ is the optimal counter strategy to $\sigma$, such that $\mathsf{val}(\sigma)=\mathsf{val}(\sigma,\tau)$. $\mathsf{Prof}(\sigma)=\{(3,4),(3,0)\}$, because both the successor to the left and the successor to the right have a better valuation, $(3,\{4\},1)$ and $(0,\emptyset,0)$, respectively, than the successor on the selected self-loop, $(3,\emptyset,0)$.

For a strategy $\sigma$ and a functional (right-unique) subsets $P\subseteq\mathsf{Prof}(\sigma)$ we define the strategy $\sigma^{P}$ with $\sigma^{P}:v\mapsto v^{\prime}$ if $(v,v^{\prime})\in P$ and $\sigma^{P}:v\mapsto\sigma(v)$ if there is no $v^{\prime}\in V$ with $(v,v^{\prime})\in P$. For a class of graph games, profitable updates are combinable if, for all strategies $\sigma$ and all functional (right-unique) subsets $P\subseteq\mathsf{Prof}(\sigma)$ we have that $\mathsf{val}_{\mathcal{G}}(\sigma^{P})\sqsupset\mathsf{val}_{\mathcal{G}}(\sigma)$. Moreover, we say that a class of graph games is maximum identifying if $\mathsf{Prof}(\sigma)=\emptyset\Leftrightarrow\mathsf{val}_{\mathcal{G}}(\sigma)=\mathsf{val}_{\mathcal{G}}$. Algorithm 4 provides a generic template for strategy improvement algorithms.

We say that a class of games is good for $\max$ strategy improvement if they are positionally determined and have combinable and maximum identifying improvements.

If a class of games is good for $\max$ strategy improvement then Algorithm 4 terminates with an optimal strategy $\sigma$ ($\mathsf{val}_{\mathcal{G}}(\sigma)=\mathsf{val}_{\mathcal{G}}$) for Player Max.

As a remark, we can drop the combinability requirement while maintaining correctness when we restrict the updates to a single position, that is, when we require $P$ to be singleton for every update. We call such strategy improvement algorithms slow, and a class of games good for slow $\max$ strategy improvement if it is maximum identifying and positionally determined.

If a class of games is positionally determined games with maximum identifying improvement then all slow strategy improvement algorithms terminate with an optimal strategy $\sigma$ ($\mathsf{val}_{\mathcal{G}}(\sigma)=\mathsf{val}_{\mathcal{G}}$) for Player Max.

The strategy improvement algorithm will produce a sequence $\sigma_{0},\sigma_{1},\sigma_{2}\ldots$ of positional strategies with increasing quality $\mathsf{val}_{\mathcal{G}}(\sigma_{0})\sqsubset\mathsf{val}_{\mathcal{G}}(\sigma_{1})\sqsubset\mathsf{val}_{\mathcal{G}}(\sigma_{2})\sqsubset\ldots$. As the set of positional strategies is finite, this chain must be finite. As the game is maximum identifying, the stopping condition provides optimality. ∎

Various concepts and results extend naturally for analogous claims about Player Min. We call a class of game good for strategy improvement if it is good for $\max$ strategy improvement and good for $\min$ strategy improvement. Parity games, mean payoff games, and discounted payoff games are all good for strategy improvement (for both players). Moreover, the calculation of $\mathsf{Prof}(\sigma)$ is cheap in all of these instances, which makes them well suited for strategy improvement techniques.

Symmetric Strategy Improvement Algorithm

We first extend the termination argument for classic strategy improvement techniques (Theorems 2.9 and 2.10) to symmetric strategy improvement given as Algorithm 5.

The symmetric strategy improvement algorithm terminates for all classes of games that are good for strategy improvement.

We first observe that the algorithm yields a sequence $\sigma_{0},\sigma_{1},\sigma_{2},\ldots$ of Player Max strategies for $\mathcal{G}$ with improving values $\mathsf{val}_{\mathcal{G}}(\sigma_{0})\sqsubseteq\mathsf{val}_{\mathcal{G}}(\sigma_{1})\sqsubseteq\mathsf{val}_{\mathcal{G}}(\sigma_{2})\sqsubseteq\ldots$, where equality, $\mathsf{val}_{\mathcal{G}}(\sigma_{i})\equiv\mathsf{val}_{\mathcal{G}}(\sigma_{i+i})$, implies $\sigma_{i}=\sigma_{i+1}$. Similarly, for the sequence $\tau_{0},\tau_{1},\tau_{2},\ldots$ of Player Min strategies for $\mathcal{G}$, the values $\mathsf{val}_{\mathcal{G}}(\tau_{0})\sqsupseteq\mathsf{val}_{\mathcal{G}}(\tau_{1})\sqsupseteq\mathsf{val}_{\mathcal{G}}(\tau_{2})\sqsupseteq\ldots$, improve (for Player Min), such that equality, $\mathsf{val}_{\mathcal{G}}(\tau_{i})\equiv\mathsf{val}_{\mathcal{G}}(\tau_{i+i})$, implies $\tau_{i}=\tau_{i+1}$. As the number of values that can be taken is finite, eventually both values stabilise and the algorithm terminates. ∎

What remains to be shown is that the symmetric strategy improvement algorithm cannot terminate with an incorrect result. In order to show this, we first prove the weaker claim that it is optimal in $\mathcal{G}(\sigma,\tau,\sigma^{c}_{\tau},\tau^{c}_{\sigma})=(V_{\max},V_{\min},E^{\prime},\mathsf{val})$ such that E^{\prime}=\big{\{}\big{(}v,\sigma(v)\big{)}\mid v\in V_{\max}\big{\}}\cup\big{\{}\big{(}v,\tau(v)\big{)}\mid v\in V_{\min}\big{\}}\cup\big{\{}\big{(}v,\sigma^{c}_{\tau}(v)\big{)}\mid v\in V_{\max}\big{\}}\cup\big{\{}\big{(}v,\tau^{c}_{\sigma}(v)\big{)}\mid v\in V_{\min}\big{\}} is the subgame of $\mathcal{G}$ whose edges are those defined by the four positional strategies, when it terminates with the strategy pair $\sigma,\tau$.

When the symmetric strategy improvement algorithm terminates with the strategy pair $\sigma,\tau$ on games that are good for strategy improvement, then $\sigma$ and $\tau$ are the optimal strategies for Players Max and Min, respectively, in $\mathcal{G}(\sigma,\tau,\sigma^{c}_{\tau},\tau^{c}_{\sigma})$.

For $\mathcal{G}(\sigma,\tau,\sigma^{c}_{\tau},\tau^{c}_{\sigma})$, both update steps are not restricted: the changes Player Max can potentially select his updates from are the edges defined by $\sigma^{c}_{\tau}$ at the vertices $v\in V_{\max}$ where $\sigma$ and $\sigma^{c}_{\tau}$ differ ($\sigma(v)\neq\sigma^{c}_{\tau}(v)$). Consequently, $\mathsf{Prof}(\sigma)=\mathsf{Prof}(\sigma)\cap\sigma^{c}_{\tau}$.

Thus, $\sigma=\sigma^{\prime}$ holds if, and only if, $\sigma$ is the result of an update step when using classic strategy improvement in $\mathcal{G}(\sigma,\tau,\sigma^{c}_{\tau},\tau^{c}_{\sigma})$ when starting in $\sigma$. As game is maximum identifying, $\sigma$ is the optimal Player Max strategy for $\mathcal{G}(\sigma,\tau,\sigma^{c}_{\tau},\tau^{c}_{\sigma})$.

Likewise, the Player Min can potentially select every updates from $\tau^{c}_{\sigma}$, at vertices $v\in V_{\min}$ and we first get $\mathsf{Prof}(\tau)=\mathsf{Prof}(\tau)\cap\tau^{c}_{\sigma}$ with the same argument. As the game is minimum identifying, $\tau$ is the optimal Player Min strategy for $\mathcal{G}(\sigma,\tau,\sigma^{c}_{\tau},\tau^{c}_{\sigma})$. ∎

We are now in a position to expand the optimality in the subgame $\mathcal{G}(\sigma,\tau,\sigma^{c}_{\tau},\tau^{c}_{\sigma})$ from Lemma 3.2 to global optimality the valuation of these strategies for $\mathcal{G}$.

When the symmetric strategy improvement algorithm terminates with the strategy pair $\sigma,\tau$ on a game $\mathcal{G}$ that is good for strategy improvement, then $\sigma$ is an optimal Player Max strategy and $\tau$ an optimal Player Min strategy.

Let $\sigma,\tau$ be the strategies returned by the symmetric strategy improvement algorithm for a game $\mathcal{G}$, and let $\mathcal{L}=\mathcal{G}(\sigma,\tau,\sigma^{c}_{\tau},\tau^{c}_{\sigma})$ denote the local game from Lemma 3.2 defined by them. Lemma 3.2 has established optimality in $\mathcal{L}$. Observing that the optimal responses in $\mathcal{G}$ to $\sigma$ and $\tau$, $\tau^{c}_{\sigma}$ and $\sigma^{c}_{\tau}$, respectively, are available in $\mathcal{L}$, we first see that they are also optimal in $\mathcal{L}$. Thus, we have

$\mathsf{val}_{\mathcal{L}}(\sigma)\equiv\mathsf{val}_{\mathcal{L}}(\sigma,\tau^{c}_{\sigma})\equiv\mathsf{val}_{\mathcal{G}}(\sigma,\tau^{c}_{\sigma})$ and

$\mathsf{val}_{\mathcal{L}}(\tau)\equiv\mathsf{val}_{\mathcal{L}}(\sigma^{c}_{\tau},\tau)\equiv\mathsf{val}_{\mathcal{G}}(\sigma^{c}_{\tau},\tau)$.

Optimality in $\mathcal{L}$ then provides $\mathsf{val}_{\mathcal{L}}(\sigma)=\mathsf{val}_{\mathcal{L}}(\tau)$. Putting these three equations together, we get $\mathsf{val}_{\mathcal{G}}(\sigma,\tau^{c}_{\sigma})\equiv\mathsf{val}_{\mathcal{G}}(\sigma^{c}_{\tau},\tau)$.

Taking into account that $\tau^{c}_{\sigma}$ and $\sigma^{c}_{\tau}$ are the optimal responses to $\sigma$ and $\tau$, respectively, in $\mathcal{G}$, we expand this to $\mathsf{val}_{\mathcal{G}}\sqsupseteq\mathsf{val}_{\mathcal{G}}(\sigma)\equiv\mathsf{val}_{\mathcal{G}}(\sigma,\tau^{c}_{\sigma})\equiv\mathsf{val}_{\mathcal{G}}(\sigma^{c}_{\tau},\tau)\equiv\mathsf{val}_{\mathcal{G}}(\tau)\sqsupseteq\mathsf{val}_{\mathcal{G}}$ and get $\mathsf{val}_{\mathcal{G}}\equiv\mathsf{val}_{\mathcal{G}}(\sigma)\equiv\mathsf{val}_{\mathcal{G}}(\tau)\equiv\mathsf{val}_{\mathcal{G}}(\sigma,\tau)$. ∎

The Lemmas in this subsection yield the following results.

The symmetric strategy improvement algorithm is correct for games that are good for strategy improvement.

The slow symmetric strategy improvement algorithm is correct for positionally determined games that are maximum and minimum identifying.

We implemented our symmetric strategy improvement algorithm based on the progress measures introduced by Vöge and Jurdziński . The first step is to determine the valuation for the optimal counter strategies to and the valuations for $\sigma$ and $\tau$.

In our running example from Figure 1, we have discussed in the previous section that $\tau$ is the optimal counter strategy $\tau^{c}_{\sigma}$ and that $\mathsf{Prof}(\sigma)=\{(3,4),(3,0)\}$. In the optimal counter strategy $\sigma^{c}_{\tau}$ to $\tau$, Player Max moves from $3$ to $4$, and we get $\mathsf{val}(1,\tau)=(1,\emptyset,0)$, $\mathsf{val}(4,\tau)=(4,\emptyset,0)$, $\mathsf{val}(3,\tau)=(4,\emptyset,1)$, and $\mathsf{val}(0,\tau)=(0,\emptyset,0)$. Consequently, $\mathsf{Prof}(\tau)=\{(4,1)\}$. For the update of $\sigma$, we select the intersection of $\mathsf{Prof}(\sigma)$ and $\sigma^{c}_{\tau}$. In our example, this is the edge from $3$ to $4$ (depicted in green). To update $\tau$, we select the intersection of $\mathsf{Prof}(\tau)$ and $\tau^{c}_{\sigma}$. In our example, this intersection is empty, as the current strategy $\tau$ agrees with $\tau^{c}_{\sigma}$.

2 A minor improvement on stopping criteria

In this subsection, we look at a minor albeit natural improvement over Algorithm 5 shown in Algorithm 6. There we used termination on both sides as a condition to terminate the algorithm. We could alternatively check if either player has reached an optimum. Once this is the case, we can return the optimal strategy and an optimal counter strategy to it.

The correctness of this stopping condition is provided by Theorems 2.9 and 2.10, and checking this stopping condition is usually cheap: it suffices to check if $\mathsf{Prof}(\sigma)$ or $\mathsf{Prof}(\tau)$ is empty. This provides us with a small optimisation, as we can stop as soon as one of the strategies involved is optimal. However this small optimisation can only provide a small advantage.

The difference in the number of iterations of Algorithm 5 and Algorithm 6 is at most linear in the number of states of $\mathcal{G}$.

Let $\sigma$ be an optimal strategy for $\mathcal{G}$. When starting with a strategy pair $\sigma,\tau_{0}$ for some strategy $\tau_{0}$ of Player Min, we first construct the optimal counter strategies $\tau^{c}_{\sigma}$ and $\sigma_{\tau_{0}}$. As $\sigma$ is optimal and $\mathcal{G}$ maximum identifying, $\mathsf{Prof}(\sigma)=\emptyset$, and strategy improvement will not change it. In particular, our algorithm will always provide $\sigma^{\prime}=\sigma$, irrespective of the optimal counter strategy $\sigma_{\tau_{i}}^{c}$ to a strategy $\tau_{i}$ of Player Min. This also implies that $\tau^{c}_{\sigma}$ will not change. It is now easy to see that, unless $\tau_{i}^{\prime}=\tau_{i}$, $\tau_{i+1}=\tau_{i}^{\prime}$ differs from $\tau_{i}$ in at least one decision, and it differs by adhering to $\tau^{c}_{\sigma}$ at the positions where it differs ($\forall v\in V_{\min}.\ \tau_{i}(v)\neq\tau_{i+1}(v)\Rightarrow\tau_{i+1}(v)=\tau^{c}_{\sigma}(v)$). Such an update can happen at most once for each Player Min position. The argument for starting with an optimal strategy $\tau$ of Player Min is similar. ∎

Friedmann’s Traps

In a seminal work on the complexity of strategy improvement , Friedmann uses a class of parity games called 1-sink parity games. These games contain a sink node with the weakest odd parity in a max-parity game. This sink node is reachable from every other node in the game and such a game is won by Player Min eventually. Figure 2 shows a lower bound game from .

In order to obtain an exponential lower bound for the classic strategy improvement algorithm with the locally optimising policy, these sink games implement a binary counter realised by a gadget called a cycle gate which consists of two components. With $n$ cycle gates, we have a representation of the $n$ bits for an $n$ bit counter. The first component of a cycle gate is called a simple cycle. In Figure 2, the three smaller boxes shown in yellow are the simple cycles of the game. These simple cycles encode the bits of the counter. The second component of the cycle gate gadget is called a deceleration lane. This structure serves to ensure that any profitable updates to strategies are postponed by cycling through seemingly more profitable improvements, in the order $r,s,a_{1},a_{2},\ldots$, before eventually turning to $e_{i}$. This structure is shown as a shaded blue rectangle in Figure 2.

A simple cycle consists of exactly one Player Max controlled node $d$ with a weak odd colour $k$ and one Player Min controlled node $e$ with the even colour $k+1$. The Player Max node is also connected to some set of external nodes in the game and the Player Min node is connected to an output node with a high even colour on a path to the sink node. Given a strategy $\sigma$, we say that a simple cycle is closed if we have an edge $\sigma(d)=e$. Otherwise, we say that the simple cycle is open. Opening and closing cycles correspond to unsetting and setting bits. We then say a cycle gate is open or closed when its corresponding simple cycle is open or closed respectively.

In these lower bound games, the simple cycles are connected to the deceleration lane in such a way that lower valued cycles have less edges entering the deceleration lane ensuring that lower open cycles close before higher open cycles. This allows the lesser significant bits to be set and reset before the higher significant bits.

The deceleration lane hides sensible improvements, thus making the players take more iterations before taking the best improvement. It is then shown in that incrementing a bit state always requires more than one strategy iteration in 4 different phases. This gadget thus counts an exponential number of improvement steps taken by the strategy improvement algorithm to flip $n$ bits. For a detailed exposition of the gadget and the exponential lower bound construction, we refer the reader to .

We discuss the effect of symmetric strategy improvement on Friedmann’s traps, with a focus on the simple cycles. Simple cycles are the central component of the cycle gates and the heart of the lower bound proof. As described above, an $n$-bit counter is represented by $n$ cycle gates, each cycle gate embedding a smaller simple cycle. These simple cycles are reused exponentially often to represent $n$ bits. Both players have the choice to open or close the simple cycles.

The optimal strategy of both players in the simple cycles of Figure 2 is to turn right. (For Player Max, one could say that he wants to leave the cycle, and for Player Min, one could say that she wants to stay in it.) When the players agree to stay in the cycle, Player Max wins the parity game. In fact these are the only places where Player Max can win positionally in this parity game. When running the symmetric strategy improvement algorithm for Player Max, the optimal counter strategy by Player Min is to move to the right in simple cycles where Player Max is moving to the right, and to move left in all other simple cycles.

As mentioned before, Friedmann showed that, when looking at an abstraction of the Player Max strategy that only distinguishes the decisions of turning right or not turning right in the simple cycles, then they essentially behave like a binary counter that, with some delay (caused by the deceleration lane) will ‘count up’. More precisely, one step after the $i^{th}$ bit has been activated, all lower bits are reset.

We now discuss how symmetric strategy improvement can beat this mechanism by taking the view of both players into account. For this, we consider a starting configuration, where Player Min moves to the right in the $j$ most significant simple cycle positions, where $j$ can be . Note that, when Player Min moves right in all of these positions, she has found her optimal strategy and we can invoke Theorem 3.7 to show that the algorithm terminates in a linear number of steps—or simply stop when using the alternative stopping condition.

The first observation is that changing the decision to moving left will not lead to an improvement, as it produces a winning cycle of a quality (leading even colour) higher than the quality of any cycle available for Player Max under the current strategy of Player Min. Let us now consider the less significant position $j+1$. First, we observe that moving to the right is a superior strategy. This can easily be seen: moving to the left produces a cycle with a dominating even colour and thus turns out to be winning for Player Max. Moving to the right in position $j+1$ and (by our assumption) all more significant positions removes this cycle and implies that the leading colour from this position is 1. This is clearly better for Player Min. If Player Min uses a strategy where $j+1$ is the most significant position where she decides to move to the left, we have the following case distinctions for Player Max’s strategy in this simple cycle:

Player Max moves to the right in this simple cycle. Then moving to the right is also the optimal counter strategy for Player Min, and her strategy will be updated accordingly.

Player Max does not move right in this simple cycle with her current strategy $\sigma$. Moving right in this simple cycle is among $\mathsf{Prof}(\sigma)$, as one even colour is added to the set in the quality measure in the local comparison. It is also the choice for the optimal counter strategy $\sigma^{c}_{\tau}$ to the current strategy $\tau$ of Player Min, as this is the only way for Player Max to produce a valuation with the dominating even colour of this simple cycle, while to valuation with a higher even colour is possible.

Taking these two cases into consideration, Player Min will move to the right in the $j$ most significant positions after $2j$ improvement steps. When Player Max has found his optimal strategy, we can invoke Theorem 3.7 to show termination in linear steps for the algorithm.

There are similar arguments for all kinds of traps that Friedmann has developed for strategy improvement algorithms. We have not formalised these arguments on other instances, but provided the number of iterations needed by our symmetric strategy improvement algorithm for all of them in the next section.

Note that the way in which Friedmann traps asymmetric strategy improvement has proven to be quite resistant to the improvement policy (snare , random facet , globally optimal , etc.). From the perspective of the traps, the different policies try to aim at a minor point in the mechanism of the traps, and this minor point is adjusted. The central mechanism, however is not affected. All of these examples have some variant of simple cycles at the heart of the counter and a deceleration lane to orchestrate the timely counting.

Symmetric strategy improvement aims at the mechanism of the traps themselves. It seems that examples that trap symmetric strategy improvement algorithms need to do more than just trapping both players (which could be done by copying the trap with inverse roles), they need to trap them simultaneously. It is not likely to find a proof that such traps do not exist, as this would imply a proof that symmetric strategy improvement solves parity (or, depending on the proof, mean or discounted payoff) games in polynomial time. But it seems that such traps would need a different structure. A further difference to asymmetric strategy improvement is that the deceleration lane ceases to work.

Taking into account that finding traps for asymmetric strategy improvement took decades and was very insightful, this looks like an interesting challenge for future research.

Experimental Results

We have implemented the symmetric strategy improvement algorithm for parity games and compared it with the standard strategy improvement algorithm with the popular locally optimising and other switching rules. To generate various examples we used the tools steadygame and stratimprgen that comes as a part of the parity game solver collection PGSolver . We have compared the performance of our algorith on parity games with 100 positions (see appendix) and found that the locally optimising policy outperforms other switching rules. We therefore compare our symmetric strategy improvement algorithm with the locally optimising strategy improvement below.

Since every iteration of both algorithms is rather similar—one iteration of our symmetric strategy improvement algorithm essentially runs two copies of an iteration of a classical strategy improvement algorithm—and can be performed in polynomial time, the key data to compare these algorithms is the number of iterations taken by both algorithms.

Symmetric strategy improvement will often rule out improvements at individual positions: it disregards profitable changes of Player Max and Min if they do not comply with $\sigma^{c}_{\tau}$ and $\tau^{c}_{\sigma}$, respectively. It is well known that considering fewer updates can lead to a significant increase in the number of updates on random examples and benchmarks. An algorithm based on the random-facet method , e.g., needs around a hundred iterations on the random examples with 100 positions we have drawn, simply because it updates only a single position at a time. The same holds for a random-edge policy where only a single position is updated. The figures for these two methods are given in the appendix.

It is therefore good news that symmetric strategy improvement does not display a similar weakness. It even uses less updates when compared to classic strategy improvement with the popular locally optimising and locally random policy rules. Note also that having less updates can lead to a faster evaluation of the update, because unchanged parts do not need to be re-evaluated .

As shown in Figure 3, the symmetric strategy improvement algorithm not only performs better (on average) in comparison with the traditional strategy improvement algorithm with the locally optimising policy rule, but also avoids Friedmann’s traps for the strategy improvement algorithm. The following table shows the performance of symmetric strategy improvement algorithm for Friedmann’s traps for other common switching rules. It is clear that our algorithm is not exponential for these classes of examples.

Discussion

We have introduced symmetric approaches to strategy improvement, where the players take inspiration from the respective other’s strategy when improving theirs. This creates a rather moderate overhead, where each step is at most twice as expensive as a normal improvement step. For this moderate price, we have shown that we can break the traps Friedmann has introduced to establish exponential bounds for the different update policies in classic strategy improvement .

In hindsight, attacking a symmetric problem with a symmetric approach seems so natural, that it is quite surprising that it has not been attempted immediately. There are, however, good reasons for this, but one should also consent that the claim is not entirely true: the concurrent update to the respective optimal counter strategy has been considered quite early , but was dismissed, because it can lead to cycles .

The first reason is therefore that it was folklore that symmetric strategy improvement does not work. The second reason is that the argument for the techniques that we have developed in this paper would have been restricted to beauty until some of the appeal of classic strategy improvement was caught in Friedmann’s traps. Friedmann himself, however, remained optimistic:

We think that the strategy iteration still is a promising candidate for a polynomial time algorithm, however it may be necessary to alter more of it than just the improvement policy.

This is precisely, what the introduction of symmetry and co-improvement tries to do.

References