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


Reports on

Research blog

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:

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$:
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.)
This holds for any positional condition (ex: parity and mean payoff)!

Results


Theorem: (Czerwiński, Daviaud, F., Jurdziński, Lazić, and Parys) 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$) Corollary: Algorithm $O(n m (nB)^{1 - 1/n})$

Theorem: (parameter: number of weights $k$) Corollary: Algorithm $O(m n^k)$