Value iteration for parity games

We use the notion of universal trees introduced in this post and the fundamental theorem proved in this post.

We refer to this paper for full details.

Progress measures and universal trees

We fix two parameters n and d, and T a universal tree.

Definition:
Consider a parity game \mathcal{G} with n vertices and priorities in [0,d-1]. A progress measure \mathcal{G} is a function \mu : V \to T \cup \{\bot\} such that
* if v \in V_E, then there exists (v,p,v’) \in E such that \mu(v) \vartriangleleft_p \mu(v’)
* if v \in V_A, then for all (v,p,v’) \in E we have \mu(v) \vartriangleleft_p \mu(v’)

We can now state the main theorem underlying the value iteration algorithm.

Theorem:
For all parity games with n vertices and priorities in [0,d-1], there exists a progress measure such that \mu(v) \neq \bot if and only if Eve has a winning strategy from v.

Proof:
This is an easy corollary of the fundamental theorem combined with positional determinacy.

First, observe that for any progress measure \mu, we can define a positional strategy \sigma by defining \sigma(v) = (v,p,v’) such that \mu(v) \vartriangleleft_p \mu(v’). Now reducing to the vertices such that \mu(v) \neq \bot and the moves prescribed by \sigma we obtain a graph together with a progress measure for this graph. It follows that \sigma is a winning strategy from all vertices such that \mu(v) \neq \bot. Note that this observation holds for any progress measure \mu.

Conversely, assume that Eve has a winning strategy from v, and let \sigma be a positional winning strategy. Consider the graph \mathcal{G}[\sigma], it satisfies parity, hence by the fundamental theorem there exists a progress measure. Combined with the strategy \sigma this yields a progress measure for the game \mathcal{G}.

The algorithm

The value iteration algorithm constructs the largest progress measure. It manipulates functions \mu : V \to T \cup \{\bot\}. The initial function assigns all vertices to the maximal (i.e., rightmost) leaf in T. At each step, the value iteration algorithm picks a vertex v, and checks whether the local conditions are satisfied by \mu for v. If they are not, the value of \mu(v) is decreased by the minimal possible amount to satisfy them, giving rise to \textrm{lift}_v(\mu). If this is not possible, \mu(v) is assigned \bot (losing).

The correctness follows from the two observations: let \mu_{\star} be a labeling as in the theorem above, for the order \vartriangleleft_0:
* the initial labeling is pointwise larger than \mu_{\star},
* if \mu is pointwise larger than \mu_{\star}, then so is \textrm{lift}_v(\mu).

Complexity

The algorithm given above lifts a vertex v at most |T| many times, which is the number of leaves of T. Hence the total number of lifts is O(n |T|), hence so is (roughly) the complexity of the algorithm, provided lifts can be performed in reasonable time (which is the case when the universal tree is reasonably described).

Theorem: (Jurdziński and Lazić, 2017)
There exists a (n,h)-universal tree with n^{\log(h)} leaves

This yields the succinct progress measure algorithm of Jurdziński and Lazić.

Corollary:
There exists a quasipolynomial time algorithm solving parity games