Nathanaël Fijalkow
CNRS, LaBRI, Bordeaux, and The Alan Turing Institute of data science, London
Universal graphs for parity and mean payoff games
Main objectives
- introduce the notion of universal graphs and their applications to games
- give a simple and unified presentation of all three quasipolynomial time algorithms for parity games
- construct new algorithms for mean payoff games
- show tight lower bounds for the construction of algorithms in this framework for both parity and mean payoff games
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) and $d$ (number of priorities)
Best algorithms (Calude, Jain, Khoussainov, Li, and Stephan STOC best paper award 2017, then Jurdziński and Lazić 2017, then Lehtinen 2018)
$$O(n^{\log(d)}) = O(d^{\log(n)})$$
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}$!
Mean payoff games
Mean payoff: the average limit is
non negative
Solving mean payoff games
INPUT: A mean payoff 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), $B$ (largest weight), $k$ (number of different weights)
Best algorithms (Zwick and Paterson 1996, Brim et al 2011)
$$O(n m B)$$
Parity games as mean payoff games
Parity: the maximal priority appearing infinitely often is even
Mean payoff: the average limit is non negative
Replace priority $p$ by $(-n)^p$:
- priority $1$ becomes weight $-n$
- priority $2$ becomes weight $n^2$
- priority $3$ becomes weight $-n^3$
Key idea: in a cycle (of length $n$) only the largest weight matters
Positional strategy
$$\sigma : V \to E$$
Theorem: If Eve has a winning strategy in a mean payoff game, she also has a positional winning strategy. The same holds for Adam.
Separating automata
Definition: A graph satisfies parity if all paths in the graph satisfy parity (eq: all cycles have maximal even priority)
$$\text{Parity}_n = \bigcup \left\{ \text{Paths}(G) : \begin{array}{c} G \text{ is an } (n,d)\text{-graph} \\ \text{satisfying parity}\end{array} \right\}.$$
Definition: A deterministic safety automaton $\mathcal{A}$ reading $[1,d]^\omega$ is parity separating if
$$\text{Parity}_n \subseteq L(\mathcal{A}) \subseteq \text{Parity}$$
Reduction to safety games
Let $G$ parity game, $A$ parity separating automaton recognising $L$.
Lemma: Eve has strategy ensuring parity if and only if she has a strategy ensuring $L$
Algorithm: Solve the safety game $G \times A$, complexity $m \cdot |A|$
Lemma: Eve has strategy ensuring parity if and only if she has a strategy ensuring $L$
Proof:
If Eve has a strategy ensuring parity, she has a positional one. Then $G_{\sigma}$ satisfies parity, so $\sigma$ ensures $L$
because $\text{Parity}_n \subseteq L$.
If Eve has a strategy ensuring $L$ then this strategy ensures parity because $L \subseteq \text{Parity}$.
Equivalence
Theorem: (Colcombet, F.)
- A universal graph induces a separating automaton of the same size
- A separating automaton induces a universal graph of the same size
This holds for any
positional condition (ex: parity and mean payoff)!
Results
Theorem: (Czerwiński, Daviaud, F., Jurdziński, Lazić, and Parys)
- There exists a quasipolynomial parity separating automaton (three constructions, one for each quasipolynomial time algorithm)
- All parity separating automata have at least quasipolynomial size
Equivalently: universal graphs
Universal trees
Definition: A tree is
$(n,h)$-universal if it embeds all trees of height $h$ with $n$ leaves
$\qquad$
Fact: Universal trees are exactly maximal universal graphs!
Universal graphs
Definition: A graph
satisfies mean payoff if all paths in the graph satisfy mean payoff (eq: no negative cycles)
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)$-MP universal if
- it satisfies mean payoff
- all graphs of size $n$ with weights in $W$ satisfying mean payoff can be homomorphically mapped into $U$
Lemma: (parameter:
maximal weight $B$)
This graph U is $(n,[-B,B])$-MP universal:
$$\phi : G \to U \text{ defined by } \phi(v) = \text{dist}(v_0,v)$$
Key idea: if $(v,w,v') \in E$, then $\text{dist}(v_0,v') \le \text{dist}(v_0,v) + w$
Corollary: Algorithm $O(n m B)$ (matches best known so far)
Results
Theorem: (parameter:
maximal weight $B$)
- There exists a universal MP graph of size $2n (nB)^{1 - 1/n}$
- All universal MP graphs have size at least $B^{1 - 1/n}$
Corollary: Algorithm $O(n m (nB)^{1 - 1/n})$
Theorem: (parameter:
number of weights $k$)
- There exists a universal MP graph of size $n^k$
- All universal MP graphs have size at least $n^{k - 2}$
Corollary: Algorithm $O(m n^k)$