Nathanaël Fijalkow
CNRS, LaBRI, Bordeaux, and The Alan Turing Institute of data science, London
Parity games: the quasipolynomial era
Universal trees
Question: what is the smallest tree containing all trees of height $2$ with $5$ leaves?
$\qquad$
Definition: A tree is $(n,h)$-universal if it contains all trees of height $h$ with $n$ leaves
Theorem:
- There exists a $(n,h)$-universal tree of size $\binom{h + \log(n)}{h}$
- This upper bound is asymptotically tight
Remark: the number $\binom{h + \log(n)}{h}$ is
- $O(n^{\log(h)})$ in general
- $n^{O(1)}$ for $h = O(\log(n))$
Upper bounds
We construct a $(n,h)$-universal tree.
Inductively
- $T_\text{middle}$ a $(n,h-1)$-universal tree
- $T_\text{left}$ a $(\lfloor n/2 \rfloor,h)$-universal tree
- $T_\text{right}$ a $(n - 1 - \lfloor n/2 \rfloor,h)$-universal tree
Fact: there exists a
balanced node
Lower bounds
$$g(n,h) = \sum_{d = 1}^n g(\lfloor n / d \rfloor,h-1)$$
Let $T$ a $(n,h)$-universal tree and $\delta \in [1,n]$.
Claim: the number of nodes at depth $h-1$ of degree $\ge \delta$ is at least $g(\lfloor n / \delta \rfloor,h-1)$.
Claim: $T_\delta$ is $(\lfloor n / \delta \rfloor,h-1)$-universal
Parity games
Parity: the maximal priority appearing infinitely often is
even
Solving parity games
INPUT: A parity game and initial vertex $v_0$
QUESTION: Does Eve have a winning strategy from $v_0$?
Parameters: $n$ (number of vertices), $m$ (number of edges) and $d$ (number of priorities)
Best algorithm
$$O \left( m \cdot \binom{d/2 + \log(n)}{d/2} \right) = O(n^{\log(d)})$$
Why might you care?
Parity games play a crucial role in:
- LTL synthesis
- automata and logic over infinite trees (emptiness games)
- modal mu-calculus (model-checking games)
But also complexity: in $\textrm{NP} \cap \textrm{coNP}$, not known to be in $\textrm{P}$!
Also: included in mean payoff, discounted payoff, and simple stochastic games
Positional strategy
$$\sigma : V \to E$$
Theorem: If Eve has a winning strategy in a parity game, she also has a positional winning strategy. The same holds for Adam.
Definition: A graph
satisfies parity if all paths in the graph satisfy parity
Remark: If $\sigma$ is a positional winning strategy, then $G_{\sigma}$ satisfies parity
Value iteration
Büchi: parity with priorities $1$ and $2$
Lemma: A graph satisfies Büchi if and only if there exists a progress measure $\mu : V \to \mathbb{N}$:
$$(v,1,v') \in E \implies \mu(v) < \mu(v')$$
A tree is the graphical representation of nested orders $\triangleleft_p$, for $p \in [1,d]$.
Example:
$\qquad$
Lemma: A graph satisfies parity if and only if there exists a tree $T$ and $\mu : V \to T$:
$$(v,p,v') \in E \implies \mu(v) \triangleleft_p \mu(v')$$
$G$ parity game.
A
progress measure is $\mu : V \to T \cup \{ \bot \}$:
$$
\begin{array}{c}
\forall v \in V_{\text{Eve}},\ \exists (v,p,v') \in E \wedge \mu(v) \triangleleft_p \mu(v') \\
\forall v \in V_{\text{Adam}},\ \forall (v,p,v') \in E,\ \mu(v) \triangleleft_p \mu(v')
\end{array}
$$
Theorem: There exists a tree $T$ and a progress measure $\mu : V \to T \cup \{ \bot \}$ such that $\mu(v) \neq \bot$ if and only if Eve wins from $v$
Corollary: Let $\mathcal{T}$ a $(n,d/2)$-universal tree.
There exists a progress measure $\mu : V \to \mathcal{T} \cup \{ \bot \}$ such that $\mu(v) \neq \bot$ if and only if Eve wins from $v$
Key idea: The value iteration algorithm constructs the
largest progress measure
Three similar stories
good for small games, value iteration, and fixed point are families of algorithms for parity games,
parametrised by the choice of a universal tree!
Beyond parity
Definition: A graph
satisfies W if all paths in the graph satisfy $W$
Definition: A (graph) homomorphism is $\phi : V \to V'$ st
$$(v,w,v') \in E \Longrightarrow (\phi(v),w,\phi(v')) \in E$$
Definition: A graph $U$ is
$(n,W)$-universal if
- it satisfies $W$
- all graphs of size $n$ satisfying $W$ can be homomorphically mapped into $U$
Value iteration algorithm
Let $G$ game with objective $W$ and $U$ a $(n,W)$-universal graph
We construct a value iteration algorithm of time complexity $m |U|$ and space complexity $n \log |U|$.
Happening now
with
universal graphs
- New algorithms for mean payoff games (F., Gawrychowski, Ohlmann)
- Logical implications (Dawar, F., Lehtinen)
- Combining parity with other objectives (Anand, F., Leroux)
- Combination of mean payoff objectives