Parity games and universal graphs
This post introduces the notion of universal graphs and their applications to parity games.
The goal of this post is to prove the main result of this paper, meaning that separating automata have at least quasipolynomial size.
This quasipolynomial barrier subjects all three quasipolynomial time algorithms for parity games as explained in the post about separating automata.
This post relies on the previous post about the fundamental theorem for parity games. All details can be found in this technical report which is a joint work with Thomas Colcombet.
Universal graphs
We fix $n,d$ two parameters.
Definition: A graph is universal if it satisfies parity and any graph of size $n$ satisfying parity can be mapped homomorphically into it.
In the remainder of this post we prove the following theorem:
Theorem: The following quantities are equal
- The size of the smallest universal tree
- The size of the smallest separating automaton
- The size of the smallest universal graph
We refer to this post for the definition of universal trees and this post for the definition of separating automata.
Thanks to the upper and lower bounds for universal trees (see this post) we know that the above quantity is quasi-polynomial.
The equivalence between universal trees and separating automata was originally proved in this paper. The innovations of the new paper is to use a different route, using universal graphs and the fundamental theorem.
The outline is as follows.
- construction from a universal graph to a universal tree
- construction from a universal tree to a separating automaton
- construction from a separating automaton to a universal graph
Universal graph to universal tree
Lemma A maximal universal graph is a universal tree.
This is an easy corollary of the lemma proved in this post which says that a maximal graph is a tree. It follows that from a universal graph, one constructs a universal tree by taking a saturation of the universal graph, which preserves the size.
Universal tree to separating automaton
Let $T$ be a universal tree. We construct an automaton $\A$ as follows. The set of states is the set of leaves of $T$. The initial state is the minimum element for the total order $E_0$. The transition function is defined as follows.
\[\delta(v,i) = \min_{E_0} \set{v' : (v,i,v') \in E}\]Note that $\A$ is deterministic.
Lemma: The automaton $\A$ is separating.
Proof: Consider a graph $G$ of size $n$ satisfying parity, we show that $\A$ accepts all paths in $G$. Thanks to the fundamental theorem, there exists a tree and a homomorphism $\phi : G \to t$.
We show by induction that for a finite path $\rho$ in $G$ ending in $v$, we have $(\delta(\pi(\rho)), 0, \phi(v)) \in E$. To initialise we recall that the initial state is the minimal element for $E_0$. For the inductive case let $\rho’ = \rho \cdot (v,i,v’)$, we are looking at $\delta(\pi(\rho’)) = \delta(\delta(\pi(\rho)),i)$. Since $(v,i,v’) \in E$ we have $(\phi(v),i,\phi(v’)) \in E$, and by induction hypothesis we have $(\delta(\pi(\rho)), 0, \phi(v)) \in E$, the combination of this implies that $(\delta(\pi(\rho)), i, \phi(v’)) \in E$. It follows by definition of $\delta$ that $(\delta(\pi(\rho’)), 0, \phi(v’)) \in E$.
To see that the automaton rejects all paths not satisfying parity, consider a path $\rho$ with odd maximal priority $i$. We note that for any state $v$ we have $(v,i,\delta(v,\pi(\rho))) \in E$, which is easily shown by induction. Since a path not satisfying parity contains a suffix consisting of infinitely many paths each of which has odd maximal priority $i$, it follows that the automaton eventually rejects such a path. Indeed, $i$ being odd $E_i$ is a non-reflexive preorder, so the sequence of states at the beginning of each loop would be an infinite increasing sequence of states.
Separating automaton to universal graph
Let $\A$ be a separating automaton. We write $\delta(u)$ for the state reached after reading the word $u$ in $\A$ from the initial state; note that $\delta(u)$ might be undefined. Without loss of generality all states in $\A$ are reachable. We construct a graph $G$ as follows. The set of vertices is the set of states of $\A$, and $(v,i,v’) \in E$ if $v’ = \delta(v,i)$.
Lemma: The following two properties hold.
- $G$ satisfies parity
- Any saturation of $G$ is universal
Proof: To see that $G$ satisfies parity, we observe that all cycles of $G$ are even, since otherwise $\A$ would accept a word not satisfying parity. We consider a saturation of $G$ which for the sake of simplicity we also call $G$. Recall that thanks to a lemma proved in this post, we know that the relation $E_0$ is a total order.
Let $H$ be a graph satisfying parity of size $n$, we construct a homomorphism $\phi$ from $H$ to $G$. We need to associate to any vertex $v$ of $H$ a vertex $\phi(v)$ of $G$. Define
\[\phi(v) = \max_{E_0} \set{\delta(\pi(\rho)) : \rho \text{ path of } H \text{ ending in } v},\]where $\pi(\rho)$ projects the path $\rho$ onto a sequence of priorities. Note that since $H$ satisfies parity, for each path $\rho$ of $H$ we have that $\delta(\pi(\rho))$ is well defined.
We verify that $\phi$ is a homomorphism. Let $(v,i,v’) \in E$, we show that $(\phi(v),i,\phi(v’)) \in E$. By definition $\phi(v) = \delta(\pi(\rho))$ for $\rho$ some path ending in $v$. Note that $\rho’ = \rho \cdot (v,i,v’)$ is a path ending in $v’$, so by definition $(\delta(\pi(\rho’)),0,\phi(v’)) \in E$. Since $\delta(\pi(\rho’)) = \delta(\delta(\pi(\rho)),i)$ and $\phi(v) = \delta(\pi(\rho))$ we have $(\phi(v),i,\delta(\pi(\rho’))) \in E$. It follows thanks to the first property of trees that $(\phi(v),i,\phi(v’)) \in E$.