\section{Analysis of the function $F$}
\label{sec:analysis_F}

Define $F(p,h) = f(2^p,h)$ for $p \ge 0$ and $h \ge 1$.
Then we have
$$\begin{array}{lll}
F(p,h) & \le & F(p,h-1) + 2 F(p-1,h), \\
F(p,1) & = & 2^p, \\
F(0,h) & = & 1.
\end{array}$$
To obtain an upper bound on $F$ we define $\overline{F}$ by
$$\begin{array}{lll}
\overline{F}(p,h) & = & \overline{F}(p,h-1) + 2 \overline{F}(p-1,h), \\
\overline{F}(p,1) & = & 2^p, \\
\overline{F}(0,h) & = & 1,
\end{array}$$
so that $F(p,h) \le \overline{F}(p,h)$.
Define the bivariate generating function 
\[
\mathcal{F}(x,y) = \sum_{p \ge 0, h \ge 1} \overline{F}(p,h) x^p y^h.
\]
Plugging the inductive equalities we obtain
\[
\mathcal{F}(x,y) = \frac{y}{1 - 2x - y},
\]
from which we extract that $\overline{F}(p,h) = 2^p \binom{p+h-1}{p}$, implying $F(p,h) \le 2^p \binom{p+h-1}{p}$.
Putting everything together we obtain
\[
f(n,h) \le 2^{\lceil \log(n) \rceil} \cdot \binom{\lceil \log(n) \rceil + h - 1}{\lceil \log(n) \rceil}.
\]

\section{Analysis of the function $G$}
\label{sec:analysis_G}

Define $G(p,h) = g(2^p,h)$ for $p \ge 0$ and $h \ge 1$.
Then we have
$$\begin{array}{lll}
G(p,h) & \ge & \sum_{k = 0}^p G(p-k,h-1), \\
G(p,1) & \ge & 1, \\
G(0,h) & = & 1.
\end{array}$$
To obtain a lower bound on $G$ we proceed similarly as for $F$.
We define $\overline{G}$ by
$$\begin{array}{lll}
\overline{G}(p,h) & = & \overline{G}(p,h-1) + \overline{G}(p-1,h), \\
\overline{G}(p,1) & = & 1, \\
\overline{G}(0,h) & = & 1,
\end{array}$$
so that $G(p,h) \ge \overline{G}(p,h)$.
We verify by induction that $\overline{G}(p,h) = \binom{p+h-1}{p}$, which follows from the identity
\[
\binom{p+h-1}{p} = \binom{p+h-2}{p} + \binom{p+h-2}{p-1}.
\]
This implies that $G(p,h) \ge \binom{p+h-1}{p}$.
Putting everything together we obtain
\[
g(n,h) \ge \binom{\lfloor \log(n) \rfloor + h - 1}{\lfloor \log(n) \rfloor}.
\]


\newpage 

\section{Pseudo-code for linear time algorithm solving safety games}\label{sec:safety}

\begin{algorithm*}
 \KwData{A safety game $\mathcal{G}=(V,E)$}
 \SetKwFunction{FUpd}{Upd}
 \SetKwFunction{FSolve}{Solve}
 \SetKwProg{Fn}{Function}{:}{}
 \DontPrintSemicolon
 
\Fn{\FSolve{$\mathcal{G}$}}{
	$X \gets V$ \;
	$R \gets \{v \in \text{V}_{\text{Eve}} \mid v \text{ is a sink}\}$ \;
	\For{$v \in \text{V}_{\text{Eve}}$}{	
		$\texttt{Count}(v) \gets $ number of edges outgoing from $v$
	}
	\vskip1em
	\While{$R \neq \emptyset$}{
		$R \gets \FUpd(X,R,\texttt{Count})$
	}
	\Return{$X$}
}

\vskip1em
\Fn{\FUpd{$X,R,\texttt{Count}$}}{
	$R' \gets \emptyset$ \;
	\For{edge $e=(v,v')$ from $X$ to $R$}{
		\If{$v \in \text{V}_{\text{Adam}}$}{
			$R' \gets R' \cup \{v\}$
		}
	}
	\Else{
		$\texttt{Count}(v) = \texttt{Count}(v) -1$ \;
		\If{$\texttt{Count}(v) = 0$}{
			$R' \gets R' \cup \{v\}$
		}
	}
	$X \gets X \setminus R'$ \;
	\Return{$R'$}
}
\caption{A linear time algorithm for solving safety games. Note that the procedure $\texttt{Upd}$, which computes $X_{i+1}$ and $R_i$ from $X_i$ and $R_{i-1}$, updates $X$ and $\texttt{Count}$ in place.}
\label{algo:value_iteration}
\end{algorithm*}

\newpage

\section*{Pseudo-code for generic value iteration algorithm}
\label{sec:product_safety}

\begin{algorithm*}[h]
 \KwData{A game $\mathcal{G}=(V,E)$ and a linear graph $\mathcal{A}=(Q,\Delta)$.}
 \SetKwFunction{FUpd}{Upd}
 \SetKwFunction{FSolve}{Solve}
 \SetKwProg{Fn}{Function}{:}{}
 \DontPrintSemicolon
 
\Fn{\FSolve{$\mathcal{G}, \mathcal{A}$}}{
	\For{$v \in V$}{
        $\theta(v) \leftarrow \min Q$
	}

	\For{$v \in \text{V}_{\text{Eve}}$}{
        $\texttt{Count}(v) \leftarrow |\{(v,c,v') \in E \mid \theta(v') \leq \delta(\theta(v),c)\}|$
	}

	$\mathrm{Inv} \leftarrow \{v \in \text{V}_{\text{Eve}} \mid \texttt{Count}(v)=0 \} \cup \{v \in \text{V}_{\text{Adam}} \mid \exists (v,c,v') \in E, \theta(v') > \delta(\theta(v),c)\}$ \;
	\vskip1em
	
	\While{$\mathrm{Inv} \neq \emptyset$}{
		$\mathrm{Inv} \leftarrow \FUpd(\theta, \mathrm{Inv}, \texttt{Count})$
	}
	\Return{$\{v \in V \mid \theta(v) < \top\}$}
}

\vskip1em
\Fn{\FUpd{$\theta, \mathrm{Inv}, \texttt{Count}$}}{
	$\mathrm{Inv}' \gets \emptyset$ \;
	\For{$v \in \mathrm{Inv}$}{
		\If{$v \in \text{V}_{\text{Eve}}$}{$\theta'(v) \gets \min\{\rho(\theta(v'),c), (v,c,v') \in E\}$}
		\Else{$\theta'(v) \gets \max\{\rho(\theta(v'),c), (v,c,v') \in E\}$}
		\For{$e=(u,c,v) \in E$ such that $\theta(v) \leq \delta(\theta(u),c) < \theta'(v)$}{
			\If{$u \in \text{V}_{\text{Adam}}$}{
				$\mathrm{Inv}' \gets \mathrm{Inv}' \cup \{u\}$
			}
			\Else{
				$\texttt{Count}(u) \gets \texttt{Count}(u) - 1$ \;
				\If{$\texttt{Count}(u) = 0$}{
					$\mathrm{Inv}' \gets \mathrm{Inv}' \cup \{u\}$
				}
			}
		}
		$\theta(v) \gets \theta'(v)$ \;
		\If{$v \in \text{V}_{\text{Eve}}$}{
			$\texttt{Count}(v) \gets |\{(v,c,v') \in E \mid \theta(v') \leq \delta(\theta(v),c)\}|$
		}
	}
	\Return{$\mathrm{Inv}'$}
}
\caption{A generic value iteration algorithm obtained by solving the safety game $\mathcal{G} \triangleright \mathcal{A}$ when $\mathcal{A}$ is linear.}
\label{alg:product_safety_game}
\end{algorithm*}


\subsection{A general reduction of universal graphs for strongly connected graphs} 
\label{subsec:reduction_strongly_connected}
The first idea is very general, it roughly says that if we know how to construct universal graphs for strongly connected graphs,
then we can use them to construct universal graphs for general graphs.

We say that a graph $G$ is strongly connected if for every pair of vertices there exists a path from one vertex to the other.
Let us refine the notion of universal graphs.

\begin{defi}[Universal graphs for strongly connected graphs]
A graph $\mathcal U$ is $(n,\Omega)$-universal for strongly connected graphs if it satisfies $\Omega$ and all strongly connected graphs of size at most $n$ satisfying $\Omega$ map into $\mathcal U$.
\end{defi}

Let us give a first construction, which we refine later.
Let $G_1$ and $G_2$ two graphs, we define their sequential product $\langle G_1,G_2 \rangle$ as follows:
the set of vertices is $V(G_1) \cup V(G_2)$, and the set of edges is
\[
E(G_1)\ \cup\ E(G_2)\ \cup\ \left(V(G_1) \times C \times V(G_2)\right).
\]
The sequential product is extended inductively:
$\langle G_1,\dots,G_p \rangle = \langle \langle G_1,\dots,G_{p-1} \rangle, G_p \rangle$.
Intuitively, $\langle G_1,\dots,G_p \rangle$ is the disjoint union of the graphs $G_i$'s with all possible forward edges
from $G_i$ to $G_j$ for any $i < j$.

\begin{lem}
\label{lem:strongly_connected_to_general_naive}
Let $\Omega$ be a prefix independent objective, $n \in \mathbb N$, 
and $\mathcal U$ an $(n,\Omega)$-universal graph for strongly connected graphs.
Then $\mathcal U^n = \langle \underbrace{\mathcal U,\dots,\mathcal U}_{n \text{ times}} \rangle$ is an $(n,\Omega)$-universal graph.
\end{lem}

\begin{proof}
We first note that any infinite path in $\mathcal U^n$ eventually remains in one copy of $\mathcal U$. Since $\mathcal U$ satisfies $\Omega$ and by prefix independence of $\Omega$, this implies that the infinite path satisfies $\Omega$, thus so does $\mathcal U^n$.

Let $G$ be a graph satisfying $\Omega$, we show that $G$ maps into $\mathcal U$.
We decompose $G$ into strongly connected components: 
let $G_1,\dots,G_p$ be the maximal strongly connected components in $G$
indexed such that if there exists an edge from $G_i$ to $G_j$ then $i < j$.
Then $V(G)$ is the disjoint union of the $V(G_i)$'s.
Each $G_i$ is a subgraph of $G$, and since $G$ satisfies $\Omega$ then so does $G_i$.
It follows that each $G_i$ maps into $\mathcal U$, let $\phi_i$ a homomorphism $\phi_i : G_i \to \mathcal U$.

Let us define $\phi : G \to \mathcal U^n$ by $\phi(v) = \phi_i(v)$ if $v \in V(G_i)$.
We now argue that $\phi$ is a homomorphism $\phi : G \to \mathcal U^n$.
Let $e = (v,c,v') \in E(G)$, 
then either $e \in E(G_i)$, and then $(\phi(v),c,\phi(v')) \in E(\mathcal U^n)$
because $\phi_i$ is a homomorphism,
or $e$ goes from $G_i$ to $G_j$ with $i < j$, and then again $(\phi(v),c,\phi(v')) \in E(\mathcal U^n)$.
Thus $\phi$ is a homomorphism and $\mathcal U^n$ is $(n,\Omega)$-universal.
\end{proof}

In the construction above we have used the fact that $G$ decomposes into at most $n$ strongly connected components of size $n$.
We refine this argument: the total size of the strongly connected components is $n$.
The issue we are facing in taking advantage of this observation is that the sequence of sizes is not known a priori, it depends on the graph. 
To address this we use a universal sequence. 
First, here a sequence means a finite sequence of non-negative integer, for instance $(5,2,3,3)$.
The size of a sequence is the total sum of its elements, so $(5,2,3,3)$ has size $13$.
We say that $v = (v_1,\dots,v_k)$ embeds into $u = (u_1,\dots,u_{k'})$ if
there exists an increasing function $f : [1,k] \to [1,k']$ such that for all $i \in [1,k]$,
we have $v_i \le u_{f(i)}$.
For example $(5,2,3,3)$ embeds into $(4,6,1,2,4,1,3)$ but not in $(3,2,5,3,3)$.
A sequence $u$ is $n$-universal if all sequences of size at most $n$ embed into $u$.

\begin{remark}
The notion of $n$-universal sequence is equivalent to that of $(n,2)$-universal trees:
a tree of height $2$ is given by a sequence consisting of the number of leaves of each subtree of height $1$.
This explains why the constructions that follow may feel familiar after reading Section~\ref{sec:parity}.
\end{remark}

Let us define an $n$-universal sequence $u_n$, inductively on $n \in \mathbb N$.
We set $u_0 = ()$ (the empty sequence), $u_1 = (1)$, and 
$u_n$ is the concatenation of $u_{\lfloor n/2 \rfloor}$ with the singleton sequence $(n)$
followed by $u_{n - 1 - \lfloor n/2 \rfloor}$. 
Writing $+$ for concatenation, the definition reads $u_n = u_{\lfloor n/2 \rfloor} + (n) + u_{n - 1 - \lfloor n/2 \rfloor}$
Let us write the first sequences:
\[
u_2 = (1,2),\quad 
u_3 = (1,3,1),\quad
u_4 = (1,2,4,1),\quad
u_5 = (1,2,5,1,2),\quad
u_6 = (1,3,1,6,1,2), \dots
\]

\begin{lem}
The sequence $u_n$ is $n$-universal and has size $O(n \log(n))$.
\end{lem}
\begin{proof}
We proceed by induction on $n$. The case $n = 0$ is clear, let us assume that $n > 0$.
Let $v = (v_1,\dots,v_k)$ be a sequence of size $n$, we show that $v$ embeds into $u_n$.
There exists a unique $p \in [1,k]$ such that 
$(v_1,\dots,v_{p-1})$ has size smaller than or equal to $\lfloor n/2 \rfloor$
and $(v_1,\dots,v_p)$ has size larger than $\lfloor n/2 \rfloor$.
This implies that $(v_{p+1},\dots,v_k)$ has size at most $n - 1 - \lfloor n/2 \rfloor$.
By induction hypothesis $(v_1,\dots,v_{p-1})$ embeds into $u_{\lfloor n/2 \rfloor}$
and $(v_{p+1},\dots,v_k)$ embeds into $u_{n - 1 - \lfloor n/2 \rfloor}$,
so $v$ embeds into $u_n$.

The recurrence on size is $|u_n| = |u_{\lfloor n/2 \rfloor}| + n + |u_{n - 1 - \lfloor n/2 \rfloor}|$,
it implies that $|u_n|$ is bounded by $O(n \log(n))$.
\end{proof}

We now use the universal sequence to improve on Lemma~\ref{lem:strongly_connected_to_general_naive}

\begin{lem}
\label{lem:strongly_connected_to_general}
Let $\Omega$ be a positionally determined prefix independent objective and $n \in \mathbb N$.
For each $k \in [1,n]$, let $\mathcal U_k$ be a $(k,\Omega)$-universal graph for strongly connected graphs.
Let us write $u_n = (x_1,\dots,x_k)$, 
then $\mathcal U(u_n) = \langle \mathcal U_{x_1},\dots,\mathcal U_{x_k} \rangle$ is an $(n,\Omega)$-universal graph.
\end{lem}
\begin{proof}
We follow the same lines as for Lemma~\ref{lem:strongly_connected_to_general_naive}, 
in particular the same argument implies that $\mathcal U(u_n)$ satisfies $\Omega$.

Let $G$ be a graph satisfying $\Omega$, we show that $G$ maps into $\mathcal U(u_n)$.
We decompose $G$ into strongly connected components as before. 
Let us write $v = (|V(G_1)|,\dots,|V(G_p)|)$ the sequence of sizes of the components.
The sequence $v$ has size at most $n$, implying that $v$ embeds into $u_n$:
there exists an increasing function $f : [1,p] \to [1,|u_n|]$ such that
for all $i \in [1,p]$ we have $|V(G_i)| \le u_{f(i)}$.
It follows that for each $i \in [1,p]$, there exists a homomorphism $\phi_i : G_i \to \mathcal U_{f(i)}$.

Let us define $\phi : G \to \mathcal U(u_n)$ by $\phi(v) = \phi_i(v)$ if $v \in V(G_i)$.
We now argue that $\phi$ is a homomorphism $\phi : G \to \mathcal U^n$.
Let $e = (v,c,v') \in E(G)$, 
then either $e \in E(G_i)$, and then $(\phi(v),c,\phi(v')) \in E(\mathcal U(u_n))$
because $\phi_i$ is a homomorphism,
or $e$ goes from $G_i$ to $G_j$ with $i < j$, and then again $(\phi(v),c,\phi(v')) \in E(\mathcal U(u_n))$
because $f$ is increasing.
Thus $\phi$ is a homomorphism and $\mathcal U(u_n)$ is $(n,\Omega)$-universal.
\end{proof}

\begin{remark}\label{rmk:complexity_of_universal_sequences}
To appreciate the improvement of Lemma~\ref{lem:strongly_connected_to_general} over Lemma~\ref{lem:strongly_connected_to_general_naive}, 
let us consider the case where the $(k,\Omega)$-universal graph $\mathcal U_k$ for strongly connected graphs has size $\alpha k$, where $\alpha$ does not depend on $k$.
Then Lemma~\ref{lem:strongly_connected_to_general_naive} yields an $(n,\Omega)$-universal graph
of size $\alpha n^2$ while Lemma~\ref{lem:strongly_connected_to_general} brings it down to $O(\alpha n \log(n))$.

\end{remark}

\subsection{Universal graphs for disjunctions of mean payoff objectives} 
\label{subsec:universal_graphs_disjunctions_mean_payoff}
We state in the following theorem an upper bound on the construction of universal graphs for disjunctions of mean payoff objectives.

\begin{thm}
\label{thm:upper_bound_universal_graph_disj_mean_payoff}
Let $n,d,N \in \mathbb N$ and $W \subseteq \mathbb Z$ of largest weight in absolute value $N$.
There exists an $(n,\bigvee_{i \in [1,d]} \MP{W}_i)$-universal graph of size $O(n \log(n) \cdot d N)$.
\end{thm}

As suggested by the previous subsection, we first construct $(n,\bigvee_{i \in [1,d]} \MP{W}_i)$-universal graphs
for strongly connected components.
The following result shows a decomposition property.

\begin{lem}
Let $G$ be a strongly connected graph and $W \subseteq \mathbb Z$.
Assume that $G$ satisfies $\bigvee_{i \in [1,d]} \MP{W}_i$ then there exists $i \in [1,d]$ such that $G$ satisfies $\MP{W}_i$.
\end{lem}

\begin{proof}
We prove the contrapositive: assume that for all $i \in [1,d]$ the graph does not satisfy $\MP{W}_i$,
implying that for each $i \in [1,d]$ there exists a negative cycle $C_i$ around some vertex $v_i$.
By iterating each cycle an increasing number of times, we construct a path in $G$ which does not satisfy $\bigvee_i \MP{W}_i$.

To make this statement formal, we use the following property:
for any $i \in [1,d]$, any finite path $\pi$ can be extended to a finite path $\pi \pi'$ with weight $\leq -1$ on the $i$\textsuperscript{th} component.
This is achieved simply by first going to $v_i$ using strong connectedness, then iterating through cycle $C_i$ a sufficient number of times.

We then apply this process repeatedly and in a cyclic way over $i \in [1,d]$ to construct an infinite path
such that for each $i \in [1,d]$, infinitely many times the $i$-th component is less than $-1$.
This produces a path which does not satisfy $\bigvee_{i \in [1,d]} \MP{W}_i$, a contradiction.
\end{proof}

\begin{cor}
\label{cor:universal_graph_strongly_connected_graphs_disj_mean_payoff}
Let $n \in \mathbb N, W \subseteq \mathbb Z$, and $\mathcal U$ be an $(n,\MP{W})$-universal graph for strongly connected graphs.
We construct $d \cdot \mathcal U$ the disjoint union of $d$ copies of $\mathcal U$, where the $i$-th copy reads the $i$-th component.
Then $d \cdot \mathcal U$ is an $(n,\bigvee_{i \in [1,d]} \MP{W}_i)$-universal graph for strongly connected graphs. 
\end{cor}

We can now prove Theorem~\ref{thm:upper_bound_universal_graph_disj_mean_payoff}.

Thanks to Lemma~\ref{lem:upper_bounds_universal_graphs_mean_payoff}, there exists an $(n,\MP{W})$-universal graph of size $nN$.
Thanks to Corollary~\ref{cor:universal_graph_strongly_connected_graphs_disj_mean_payoff}, this implies
an $(n,\bigvee_{i \in [1,d]} \MP{W}_i)$-universal graph for strongly connected graphs of size $ndN$.
Now Lemma~\ref{lem:strongly_connected_to_general} yields an $(n,\bigvee_i \MP{W}_i)$-universal graph 
of size $O(n \log(n) \cdot d N)$ (see Remark~\ref{rmk:complexity_of_universal_sequences}).

\subsection{The complexity of solving disjunctions of mean payoff games using universal graphs}
\label{subsec:complexity_disjunctions_mean_payoff}

As in the previous case disjunction of mean payoff games were studied focussing on the objective of the opponent,
who has a conjunction of mean payoff objectives to satisfy~\cite{VelnerC0HRR15}.
Let us note here that there are actually two variants of the mean payoff objective: using infimum limit or supremum limit.
In many cases the two variants are equivalent: 
this is the case when considering mean payoff games or disjunctions of parity and mean payoff games.
However, this is not true anymore for disjunctions of mean payoff objectives, as explained in~\cite{VelnerC0HRR15}.
Our constructions and results apply using the infimum limit, and do not extend to the supremum limit

The main result related to disjunction of mean payoff games in~\cite{VelnerC0HRR15} (Theorem~6) is that the problem is in $\text{NP} \cap \text{coNP}$ and can be solved in time $O(m \cdot n^2 \cdot d \cdot N)$.
(Note that since we consider the dual objectives, the infimum limit becomes a supremum limit in~\cite{VelnerC0HRR15}.)

Combining Theorem~\ref{thm:upper_bound_universal_graph_disj_mean_payoff} with Theorem~\ref{thm:solving_product_game_linear} yields the following result.

\begin{cor}
Let $n,m,d,N \in \mathbb N$.
In the RAM model with word size $w = \log(n) + \log(N) + \log(d)$, 
there exists an algorithm for solving disjunctions of mean payoff games with weights in $(-N,N)$ 
with time complexity $O(m \cdot n \log(n) \cdot d \cdot N)$ and space complexity $O(n)$.
\end{cor}

Note that for the choice of word size, the two tasks for manipulating universal graphs, 
namely computing $\delta(q,w)$ and checking whether $q \le q'$ 
are indeed unitary operations as they manipulate numbers of order $nN$.

\subsection{Separating automata for disjunctions of parity and mean payoff objectives} 
\label{subsec:universal_graphs_disjunctions_parity_mean_payoff}

\begin{thm}
\label{thm:separating_automata_disj_parity_mp}
Let $n,d \in \mathbb N, W \subseteq \mathbb Z$, $\mathcal{A}_P$ an $(n,\mathtt{Parity}(d))$-separating automaton, and $\mathcal{A}_{MP}$ an $(n,\MP{W})$-separating automaton.
Then there exists an $(n, \mathtt{Parity}(d) \vee \MP{W})$-separating automaton of size $O(d \cdot |\mathcal{A}_P| \cdot |\mathcal{A}_{MP}|)$.
\end{thm}

\begin{proof}
Let us write $\mathcal{A}_P = (Q_P,q_{0,P},\delta_P)$ and $\mathcal{A}_{MP} = (Q_{MP},q_{0,MP},\delta_{MP})$.
We define a deterministic automaton $\mathcal{A}_{P \vee MP}$: 
the set of states is $[0,d] \times Q_P \times Q_{MP}$,
the initial state is $(d, q_{0,P}, q_{0,MP})$,
and the transition function is defined as follows:
$\delta((p,q_P,q_{MP}), (p',w))$ is equal to
\[
\begin{cases}
(\max(p,p'), q_P, q'_{MP}) & \text{ if $\delta_{MP}(q_{MP}, w)$ is defined and equal to $q'_{MP}$,} \\
(0, q'_P, q_{0,MP}) & \text{ otherwise, and $\delta_P(q_{P}, \max(p,p'))$ is defined and equal to $q'_{P}$}.
\end{cases}
\]
Intuitively: $\mathcal{A}_{P \vee MP}$ simulates the automaton $\mathcal{A}_{MP}$, storing the maximal priority seen since the last reset (or from the beginning).
If the automaton $\mathcal{A}_{MP}$ rejects, the automaton resets, which means two things:
it simulates one transition of the automaton $\mathcal{A}_{P}$ using the stored priority, 
and resets the state of $\mathcal{A}_{MP}$ to its initial state.
The automaton $\mathcal{A}_{P \vee MP}$ rejects only if $\mathcal{A}_{P}$ rejects during a reset.

We now prove that $\mathcal{A}_{P \vee MP}$ is an $(n,\mathtt{Parity}(d) \vee \MP{W})$-separating automaton.
\begin{itemize}
	\item $L(\mathcal{A}_{P \vee MP}) \subseteq \mathtt{Parity}(d) \vee \MP{W}$.
	Let $\pi$ be an infinite path accepted by $\mathcal{A}_{P \vee MP}$, we distinguish two cases by looking at the run of $\pi$.

	\begin{itemize}
		\item If the run is reset finitely many times, let us write $\pi = \pi' \pi''$
		where $\pi'$ is finite and $\pi'_{MP}$ rejected by $\mathcal{A}_{MP}$, and $\pi''$ is infinite and $\pi''_{MP}$ is accepted by $\mathcal{A}_{MP}$.
		Since $\mathcal{A}_{MP}$ satisfies $\MP{W}$, this implies that $\pi''_{MP}$ satisfies $\MP{W}$,
		so by prefix independence, $\pi_{MP}$ satisfies $\MP{W}$ hence $\pi$ satisfies $\mathtt{Parity}(d) \vee \MP{W}$.
	
		\item If the run is reset infinitely many times, we may find an infinite decomposition $\pi = \pi^1 \pi^2 \dots$
		where for each $i \in \mathbb N$, the path $\pi^i_{MP}$ is rejected by $\mathcal{A}_{MP}$, and its proper prefixes are not.
		Let $p_i$ be the maximum priority appearing in $\pi^i_{P}$, the run of $\pi$ over $\mathcal{A}_{P \vee MP}$
		induces a run of $p_1 p_2 \dots$ over $\mathcal{A}_P$.
		Since $\mathcal{A}_P$ satisfies $\mathtt{Parity}(d)$, this implies that $p_1 p_2 \dots$ satisfies $\mathtt{Parity}(d)$.
		By definition of the $p_i$'s, this implies that $\pi_P$ satisfies $\mathtt{Parity}(d)$ so a fortiori $\pi$ satisfies $\mathtt{Parity}(d) \vee \MP{W}$.
	\end{itemize}		
	
	\item $(\mathtt{Parity}(d) \vee \MP{W})^{\mid n} \subseteq L(\mathcal{A}_{P \vee MP})$.
	Let $G$ be a graph satisfying $\mathtt{Parity}(d) \vee \MP{W}$ of size at most $n$,
	we need to show that all infinite paths of $G$ are accepted by $\mathcal{A}_{P \vee MP}$.
	
	We construct a graph $G_{MP}$ over the set of colours $W$ and a graph $G_P$ over the set of colours $[0,d]$.
	Both use the same set of vertices as $G$. 
	We prove that the graph $G_{MP}$ satisfies $\MP{W}$, which is used to prove that $G_P$ satisfies $\mathtt{Parity}(d)$.
	\begin{itemize}
		\item \textbf{The graph $G_{MP}$.} 
	There is an edge $(v,w,v') \in E(G_{MP})$ if 
	there exists $p \in [0,d]$ such that $e = (v,(p,w),v') \in E(G)$,
	and either $p$ is odd or $p$ is even and $e$ is not contained in any negative cycle with maximum priority $p$.
	
	\vskip1em	
	We claim that $G_{MP}$ satisfies $\MP{W}$.
	Assume towards contradiction that $G_{MP}$ contains a negative cycle $C_{MP}$. 
	It induces a negative cycle $C$ in $G$, by definition of $G_{MP}$ necessarily the maximum priority in $C$ is odd.
	Hence $C$ is a negative odd cycle in $G$, a contradiction.
	
		\item \textbf{The graph $G_{P}$.}
	There is an edge $(v,p,v') \in E(G_P)$ if 
	there exists a path in $G$ from $v$ to $v'$ 
	with maximum priority $p$ and (whose projection on the mean payoff component is) rejected by $\mathcal{A}_{MP}$.

	\vskip1em	
	We claim that $G_{P}$ satisfies $\mathtt{Parity}(d)$.
	Assume towards contradiction that $G_P$ contains an odd cycle $C_P$.
	For each edge in this cycle there is a corresponding path rejected by $\mathcal{A}_{MP}$
	with the same maximum priority.
	Putting these paths together yields an odd cycle $C$, of maximal priority $p$, in $G$ whose projection on the mean payoff component 
	is rejected by $\mathcal{A}_{MP}$.
	Since $\MP{W}^{\mid n} \subseteq L(\mathcal{A}_{MP})$ and as we have shown, $G_{MP}$ satisfies $\MP{W}$, 
	the projection of $C$ on the mean payoff component is not in $G_{MP}$,
	so there exists an edge $(v,(p',w),v')$ in $C$ such that $(v,w,v')$ is not in $E(G_{MP})$. 
	This implies that $p'$ is even, so in particular $p' < p$, and $(v,(p',w),v')$ is contained in a negative cycle $C'$ in $G$ with maximum priority $p'$.	
	Combining the odd cycle $C$ followed by sufficiently many iterations of the negative cycle $C'$ yields a path in $G$, with negative weight, and maximal priority $p$ which is odd, a contradiction.
	\end{itemize}
			
	Let $\pi$ an infinite path in $G$, we show that $\pi$ is accepted by $\mathcal{A}_{P \vee MP}$.
	Let us consider first only the mean payoff component: we run $\pi$ repeatedly 	over $\mathcal{A}_{MP}$,
	and distinguish two cases.
	
	\begin{itemize}
		\item If there are finitely many resets, let us write $\pi = \pi_1 \pi_2 \dots \pi_k \pi'$
		where $\pi_1,\dots,\pi_k$ are paths rejected by $\mathcal{A}_{MP}$ with proper prefixes accepted by $\mathcal{A}_{MP}$ and $\pi'$ is accepted by $\mathcal{A}_{MP}$.
		To show that $\pi$ is accepted by $\mathcal{A}_{P \vee MP}$ we need to show that the automaton $\mathcal{A}_P$
		accepts the word $p_1 \dots p_k$ where $p_i$ is the maximum priority appearing in $\pi_i$ for $i \in [1,k]$.
		Indeed, $p_1 \dots p_k$ is a path in $G_P$, which is a graph of $n$ satisfying $\mathtt{Parity}(d)$,
		so $\mathcal{A}_P$ accepts $p_1 \dots p_k$.
	
		\item If there are infinitely many resets, let us write $\pi = \pi_1 \pi_2 \dots$
		where for each $i \in \mathbb N$, the path $\pi_i$ is rejected by $\mathcal{A}_{MP}$ and its proper prefixes are not.
		To show that $\pi$ is accepted by $\mathcal{A}_{P \vee MP}$ we need to show that the automaton $\mathcal{A}_P$
		accepts the word $p_1 p_2 \dots$, which holds for the same reason as the other case: 
		$p_1 p_2 \dots$ is a path in $G_P$.
	\end{itemize}		
\end{itemize}

\end{proof}

\subsection{The complexity of solving disjunctions of parity and mean payoff games using separating automata}
\label{subsec:complexity_disjunctions_parity_mean_payoff}

The class of games with a disjunction of a parity and a mean payoff objective have been introduced in~\cite{ChatterjeeHJ05},
with a twist: this paper studies the case of a conjunction instead of a disjunction, which is more natural in many applications.
This is equivalent here since both parity and mean payoff objectives are dual, in other words
if the objective of Eve is a disjunction of a parity and a mean payoff objective, then 
the objective of Adam is a conjunction of a parity and a mean payoff objective.
Hence all existing results apply here with suitable changes.
The reason why we consider the objective of the opponent is that it is positionally determined,
which is the key assumption for using the universal graph technology.

The state of the art for solving disjunctions of parity and mean payoff games is due to~\cite{DaviaudJL18},
which presents a pseudo-quasi-polynomial algorithm.
We refer to~\cite{DaviaudJL18} for references on previous studies for this class of games.
As they explain, these games are logarithmic space equivalent to the same games replacing mean payoff by energy,
and polynomial time equivalent to games with weights~\cite{ScheweWZ19}, extending games with costs~\cite{FM14}.

Combining Theorem~\ref{thm:separating_automata_disj_parity_mp} with Theorem~\ref{thm:solving_product_game_linear}
yields the following result.

\begin{thm}
Let $n,d,N \in \mathbb N$.
There exists an algorithm~\footnote{In the RAM model with word size $w = \log(n) + \log(N)$.} 
for solving disjunctions of parity and mean payoff games
with $n$ vertices, $m$ edges, weights in $(-N,N)$ and priorities in $[0,d]$
of time complexity 
\[
O\left(m d \cdot \underbrace{n \cdot \binom{\lceil \log(n) \rceil + d/2 - 1}{\lceil \log(n) \rceil}}_{\text{Parity}}
\cdot \underbrace{nN}_{\text{Mean Payoff}}
\right).
\]
and space complexity $O(n)$.
\end{thm}

Our algorithm is similar to the one constructed in~\cite{DaviaudJL18}: they are both value iteration algorithms (called progress measure lifting algorithm in~\cite{DaviaudJL18}), combining the two value iteration algorithms for parity and mean payoff games.
However, the set of values are not the same (our algorithm stores an additional priority) and the proofs are very different. 
Besides being much shorter\footnote{The only generic result we use from universal graphs here is the equivalence between $\mathcal{G}$ and $\mathcal{G} \times \mathcal{A}$ when $\mathcal{A}$ is a separating automaton.}, one advantage of our proof is that it works with abstract universal graphs for both parity and mean payoff objectives, and shows how to combine them, whereas in~\cite{DaviaudJL18} the proof is done from scratch, extending both proofs for the parity and mean payoff objectives.



\section{Introduction}
\label{sec:intro}
\input{intro}

\section{Preliminaries}
\label{sec:preliminaries}
\input{preliminaries}

\section{Reductions to safety games}
\label{sec:reductions}
\input{reductions}

\section{Equivalence via saturation}
\label{sec:saturation}
\input{saturation}

\section{Solving the product game by value iteration}
\label{sec:value_iteration}
\input{value_iteration}

\section{Parity games}
\label{sec:parity}
\input{parity}

\section{Mean payoff}
\label{sec:mean_payoff}
\input{mean_payoff}

\section{Disjunction of parity and mean payoff}
\label{sec:disj_mean_payoff_parity}
\input{disj_mean_payoff_parity}

\section{Disjunction of mean payoff}
\label{sec:disj_mean_payoff}
\input{disj_mean_payoff}

\section{Conclusions}
\label{sec:conclusions}
\input{conclusions}

\bibliographystyle{alpha}

\subsection{Subsets of the integers and saturated graphs}
\label{subsec:saturated_universal_graphs_mean_payoff}

Towards understanding their structure we study the properties of saturated graphs and show that they are better presented using subsets of the integers.
A subset of integers $A \subseteq \mathbb Z$ defines a graph $\texttt{G}(A)$ which we call an integer graph:
the set of vertices is $A$ and the set of edges is
\[
\set{(x,w,x') \in A \times W \times A : x' - x \le w}.
\]


\begin{figure}[!ht]
\centering
\includegraphics[scale=.8]{Fig/integer_graph.eps}
\caption{Edges outgoing from $2$ (in blue) and $5$ (in red) in the integer graph given by subset $A=\{-1,0,2,3,5\}$ and weights $W=\{-3,0,1,2\}$. Other edges are omitted for clarity.}
\label{fig:integer_graph}
\end{figure}

Note that the definition depends on $W$.
Integer graphs contain no negative cycles and are invariant under translations: $A$ and $A + p$ for $p \in \mathbb Z$ induce the same integer graph (up to renaming vertices).

The key yet simple observation at this point is that given a graph with no negative cycles 
we can define a distance between vertices: \\
the distance $\text{dist}(v,v')$ from a vertex $v$ to another vertex $v'$ 
is the smallest sum of the weights along a path from $v$ to~$v'$ (when such a path exists). 
Note that saturated graphs with respect to $\MP{W}$ are linear by Theorem~\ref{thm:saturated_graphs_are_linear}. 
In particular, they have a maximal element.
\begin{lem}
\label{lem:saturated_are_integer}
Let $G$ be a saturated graph and $v_0$ its maximal element.
Let 
\[
A = \set{\text{dist}(v_0,v) \mid v \in V(G)} \subseteq \mathbb N,
\]
then $G$ maps into $\texttt{G}(A)$.
\end{lem}

\begin{proof}
We show that $\phi : V(G) \to A$ defined by $\phi(v) = \text{dist}(v_0,v)$ is a homomorphism from $G$ to $\texttt{G}(A)$.
Since $v$ is maximal, by right-composition with the $0$-self-loop on $v_0$, for every vertex $v$ there is an edge $(v_0,0,v)$.
This implies that $\text{dist}(v,v_0)$ is well defined, and non-negative.
Let $(v,w,v') \in E(G)$, then $\text{dist}(v_0,v') \le \text{dist}(v_0,v) + w$ since a path from $v_0$ to $v$ induces a path from $v_0$ to $v'$ by adding $(v,w,v')$ at the end.
In other words, $\phi(v') - \phi(v) \le w$, so $\phi$ is indeed a homomorphism.
\end{proof}


The direct consequences of Lemma~\ref{lem:saturated_are_integer} is that we can restrict our attention to integer graphs.

\begin{cor}
Let $n \in \mathbb N$ and $W \subseteq \mathbb Z$.
\begin{itemize}
	\item The smallest $(n,\MP{W})$-universal graph and the smallest $(n,\MP{W})$-universal integer graph have the same size.
	\item An integer graph $\mathcal U$ is $(n,\MP{W})$-universal if and only if every integer graph of size at most $n$ maps into~$\mathcal U$.
\end{itemize}
\end{cor}
\begin{proof}
For the first item, if $\mathcal U$ is $(n,\MP{W})$-universal, without loss of generality it is saturated, 
then $\mathcal U$ maps into the integer graph constructed in Lemma~\ref{lem:saturated_are_integer}, 
so the latter is also $(n,\MP{W})$-universal.
For the second item, the direct implication is clear so we focus on the converse.
Let us assume that every integer graph of size at most $n$ maps into $\mathcal U$ and prove that $\mathcal U$ is $(n,\MP{W})$-universal.
Let $G$ be a graph of size at most $n$ satisfying $\MP{W}$, 
thanks to Lemma~\ref{lem:saturated_are_integer} it maps into an integer graph of the same size, 
which then maps into $\mathcal U$, so by composition $G$ maps into $\mathcal U$.
\end{proof}

\subsection{Upper and lower bounds for universal graphs}
\label{subsec:universal_subsets}

We now state in the following theorem upper and lower bounds on the size of universal graphs.
We present two sets of results based on $W$: the first is parametrised by the largest weight in absolute value,
and the second by the number of different weights.

\begin{thm}[Universal graphs parameterized by largest weight]\label{thm:MP_bounds_abs}
Let $n,N \in \mathbb N$, and $W=[-N,N]$.
\begin{itemize}
	\item There exist $(n,\MP{W})$-universal graphs of size $2n \cdot (nN)^{1 - 1/n}$ and of size $(n-1)N+1$.
 	\item All $(n,\MP{W})$-universal graphs have size at least $(N+1)^{1 - 1/n}$.
\end{itemize}
\end{thm}

\begin{thm}[Universal graphs parameterised by the number of weights]\label{thm:MP_bounds_card}
\hfill
\begin{itemize}
	\item For all $n \in \mathbb N$ and $W$ of cardinality $k$, there exists an $(n,\MP{W})$-universal graph of size $O(n^k)$.
	\item For all $k$ and for all $n$ large enough, there exists $W \subseteq \mathbb Z$ of cardinality $k$ such that all $(n,\MP{W})$-universal graphs have size $\Omega(n^{k-2})$.
\end{itemize}
\end{thm}

Let us start with simple upper bounds.

\begin{lem}
\label{lem:upper_bounds_universal_graphs_mean_payoff}
Let $n,N \in \mathbb N$.
\begin{itemize}
	\item The integer graph $\texttt{G}([0,(n-1)N)])$ is $(n,\MP{[-N,N]})$-universal.
	\item For every $W$ of cardinality $k$, there exists an $(n,\MP{W})$-universal graph of size $(n-1)^k$.
\end{itemize}
\end{lem}

\begin{proof}
We show both results at the same time. 

Let $G$ be a graph of size at most $n$ satisfying $\MP{W}$, 
and $\widehat{G}$ a saturation of $G$, thanks to Lemma~\ref{lem:saturated_are_integer}
$\widehat{G}$ maps into $\texttt{G}(A)$, implying that $G$ as well.

In the case where $W = [-N,N]$ we have $A \subseteq [0,(n-1)N]$ so $\texttt{G}(A)$ maps into $[0,(n-1)N]$.
This proves that the integer graph $\texttt{G}([0,(n-1)N])$ is $(n,\MP{[-N,N]})$-universal.

In the case where $|W| \leq k$ we consider the set $\Sigma_{W,n-1}$ of all sums of $\leq n-1$ weights of $W$, 
which has cardinality at most $(n-1)^k$. 
Then $A \subseteq \Sigma_{W,n-1}$ so $\texttt{G}(A)$ maps into $\texttt{G}(\Sigma_{W,n-1})$.
This proves that $\texttt{G}(\Sigma_{W,n-1})$ is $(n,\MP{W})$-universal and it has size $(n-1)^k$.
\end{proof}

We state here a simple result that we will use several times later on about homomorphisms into integer graphs.
\begin{fact}
\label{fact:equality}
Let $G$ be a graph and $\phi : G \to \texttt{G}(A)$ a homomorphism into an integer graph. 
Let us consider a cycle
$v_0w_0v_1 \cdots v_{\ell-1}w_{\ell-1}v_0$ in $G$ of total weight $0$.
Then for $i \in [0,\ell)$, we have 
$\phi(v_{i+1}) - \phi(v_i) = w_i$,
where by convention $v_\ell = v_0$.
\end{fact}

\begin{proof}
By definition of the homomorphism using the edges $(v_i,w_i,v_{i+1})$ for $i \in [0,\ell)$
\[
\begin{array}{lll}
\phi(v_1) - \phi(v_0) & \le & w_0 \\
\phi(v_2) - \phi(v_1) & \le & w_1 \\
& \ \vdots & \\
\phi(v_0) - \phi(v_{\ell-1}) & \le & w_{\ell-1}.
\end{array}
\]
Assume towards contradiction that one of these inequalities is strict. 
Summing all of them yields $0$ on both sides (because the cycle has total weight $0$), so this would imply $0 < 0$, a contradiction.
Hence all inequalities are indeed equalities.
\end{proof}

We further analyse universal graphs when $W = [-N,N]$.
We already explained in Lemma~\ref{lem:upper_bounds_universal_graphs_mean_payoff} 
how to construct an $(n,\MP{[-N,N]})$-universal graphs of size $(n-1)N+1$.
We improve on this upper bound when $N$ is exponential in $n$.

\begin{prop}
\label{prop:upper_bound_largest_weight}
There exists an $(n,\MP{[-N,N]})$-universal graph of size 
\[
2 \Big((n-1)N - \big[((n-1)N)^{1/n} - 1 \big]^n \Big) \leq 2n \cdot (nN)^{1-1/n}.
\]
\end{prop}

As discussed above, the size of this new universal graph is not always smaller than the first universal graph of size $(n-1)N+1$, 
but it is asymptotically smaller when $n^n = o(N)$.
We now give some intuition for the construction.
The first part of the proof of Lemma~\ref{lem:upper_bounds_universal_graphs_mean_payoff} shows that it suffices to embed integer graphs of the form $\texttt{G}(A)$, when $A = \set{\text{dist}(v_0,v), v \in V}$ for some graph $G$.
In the above proof, this was done by finding a large enough set of integers that includes any such $A$:
in the first case $B = [0,(n-1)N]$ and in the second case $B = \Sigma_{W,n-1}$. 
To conclude we used the fact that if $A \subseteq B$ then there exists a homomorphism from $\texttt{G}(A)$ to $\texttt{G}(B)$.

A weaker condition is the existence of $p \in \mathbb Z$ such that $A + p \subseteq B$: 
this still implies the existence of a homomorphism from $A$ to $B$.
This will allow us to remove some values from $[0,(n-1)N]$ while remaining universal. As a drawback we need to double the range to $[0,2(n-1)N)$, which explains why this new construction is not always smaller than the first one.

\begin{proof}
Let $b = ((n-1)N)^{1/n}$.
We write integers $a \in [0,2(n-1)N)$ in basis $b$, hence using $n+1$ digits written $a[i] \in [0,b)$, that is,
\[
a = \sum_{i = 0}^n a[i] b^i \sum_{i = 0}^n a[i] ((n-1)N)^{i/n} =.
\]
Note that since $a \in [0,2(n-1)N)$ the $(n+1)$\textsuperscript{th} digit is either $0$ or $1$.
We let $B$ be the set of integers in $[0,2(n-1)N)$ which have at least one zero digit among the first $n$ digits in this decomposition.
We argue that $\texttt{G}(B)$ is $(n,\MP{[-N,N]})$-universal.

Let $G$ be a graph of size at most $n$ satisfying $\MP{W}$, to show that 
$G$ maps into $\texttt{G}(B)$ we use Lemma~\ref{lem:saturated_are_integer}
and show that for $A = \set{\text{dist}(v_0,v) : v \in V(G)}$, the graph $\texttt{G}(A)$ maps into $\texttt{G}(B)$.
To this end we show that there exists $p \in \mathbb Z$ such that $p + A \subseteq B$.


Let $A = \{d_0 < \dots < d_{n-1}\} \subseteq \mathbb Z$, where $d_0 = \text{dist}(v_0,v_0)=0$, and for all $i \in [0,n-2]$, we have $1 \leq d_{i+1}- d_i \leq N.$

We choose $p$ of the form $\sum_{i = 0}^{n-1} a_i b^i$ for $a_i \in [0,b)$,
\textit{i.e.} the $(n+1)$\textsuperscript{th} digit is $0$, or equivalently $p < (n-1)N$.
Let us write $p_i = p + d_i$, for $i \in [0,n-1]$. 
We need to choose $p$ such that for every $i \in [0,n-1]$ we have $p_i \in B$.
Note that for all $i \in [0,n-1]$ it holds that $d_i \in [0,(n-1)N)$, so whatever the choice of $p \in [0,(n-1)N]$, we have $p_i \in [0,2(n-1)N)$.

We show how to choose $a_0, a_1, \dots, a_{n-1}$ in order to ensure that $p_0,p_1,\dots, p_{n-1} \in B$, that is, each have at least one digit among the first $n$ ones which is zero.
More precisely, we show by induction on $k \in [0,n-1]$ that there exist $a_0,\dots, a_k \in [0,b)$ such that for any choice of $a_{k+1}, \dots, a_{n-1} \in [0,b)$ and for all $i \in [0,k]$, the $i$-th digit $p_i[i]$ of $p_i$ is $0$. 
For $k = 0$, we let $a_0 = 0$, which yields $p_0[0] = 0$, independently of the values of $a_1, \dots, a_{n-1}$.

Let $a_0,\dots, a_{k-1}$ be such that for any choice of $a_k, \dots, a_{n-1}$, 
for any $i \in [0,k-1]$, we have $p_i[i] = 0$. 
Let $a_k \in [0,b)$ be the (unique) value such that 
$\left(\sum_{i = 0}^k a_i b^i + d_k \right)[k] = 0$. 
Let $a_{k+1}, \dots, a_{n-1} \in [0,b)$. 
By induction hypothesis, for any $i \in [0,k)$, we have $p_i[i] = 0$. 
Now
\[
p_k[k] = \left(p + d_k \right)[k]
 = \left(\sum_{i = 0}^{n-1} a_i b^i + d_k \right)[k]
 = \left(\sum_{i = 0}^{k} a_i b^i + d_k \right)[k] + \left(b^{k+1} \sum_{i = k+1}^{n-1} a_i b^{i-k}\right)[k] = 0,
\]
since both terms are zero.
This concludes the inductive construction of $p$, and the proof of universality of $B$.
Since $B$ excludes from $[0,2(n-1)N)$ exactly $2(b-1)^n$ integers (those that do not use the digit $0$ in their first $n$ digits), the size of $B$ is
\[
2 \Big((n-1)N - \big[((n-1)N)^{1/n} - 1 \big]^n \Big).
\]
\end{proof}

We now prove the lower bound of Theorem~\ref{thm:MP_bounds_abs}.

\begin{prop}
\label{prop:lower_bound_largest_weight}
Any $(n,\MP{[-N,N]})$-universal graph has size at least $(N+1)^{1 - 1/n}$.
\end{prop}

\begin{proof}
Thanks to Lemma~\ref{lem:saturated_are_integer}, we let $\mathcal U = \texttt{G}(U)$ be an $(n,\MP{[-N,N]})$-universal integer-graph given by $U \subseteq Z$. 
We construct an injective function
$f : [0,N]^{n-1} \to U^n$.
For $(w_1,\dots,w_{n-1}) \in [0,N]^{n-1}$, we consider 
$A = \{a_0,a_1, \dots a_{n-1}\} \subseteq \mathbb Z$, with $a_0=0$ and $a_j = \sum_{i=0}^j w_j$ for $j \geq 1$.

By universality, $\texttt{G}(A)$ maps into $\mathcal U$, and we let $\phi$ be such a homomorphism.
Define $f(w_1,\dots,w_{n-1})$ to be the $n$-tuple $(\phi(a_0), \phi(a_1), \dots, \phi(a_{n-1}))$ of integer in $U$ given by
\[
f(w_1, \dots, w_{n-1}) = (\phi(a_0),\phi(a_1), \dots,\phi(a_{n-1})).
\]
To see that $f$ is injective, we apply Fact~\ref{fact:equality} to each cycle of length 2 in $\texttt{G}(A)$ of the form
\[
a_{j},w_{j+1},a_{j+1},-w_j,a_j,
\]
for $j \in [0,n-2]$. This yields
\[
\begin{array}{lll}
\phi(a_1) - \phi(a_0) & = & w_1 \\
\phi(a_2) - \phi(a_1) & = & w_2 \\
& \ \vdots & \\
\phi (a_{n-1}) - \phi(a_{n-2}) & = & w_{n-1},
\end{array}
\]
and $f$ is injective.
We conclude that 
$(N+1)^{n-1} \le |\mathcal U|^n$, so $|\mathcal U| \ge (N+1)^{1 - 1/n}$.
\end{proof}

We finally present the lower bound of Theorem~\ref{thm:MP_bounds_card}.
We let 
$T = 1 + n + n^2 + \dots + n^{k-2}$
and 
\[
W = \set{1,n,n^2,\dots,n^{k-2}, - \frac{n-1}{k-1} T}.
\]
Note that $W$ has indeed cardinality $k$.

\begin{prop}
\label{prop:lower_bound_number_weights}
Let $\mathcal U$ be an $(n,\MP{W})$-universal graph.
Then 
\[
|\mathcal U| \geq \left( \frac{n-1}{(k-1)^2} \right)^{\frac{(k-1)^2}{k}}.
\]
\end{prop}

\begin{proof}
Let $\mathcal U$ be an $(n,\MP{W})$-universal graph.

We consider a class of graphs which are cycles of length $n$, and later use a subset of those for the lower bound.
Let $(w_1,\dots,w_{n-1}) \in \set{1,n,\dots,n^{k-2}}$.
The vertices are $[0,n)$. 
There is an edge $(i-1,w_i,i)$ for $i \in [1,n)$ and an edge $(n-1, -\frac{n-1}{k-1} T, 0)$.
To make the total weight in the cycle equal to $0$,
we assume that each $n^j$ appears exactly $\frac{n-1}{k-1}$ many times in $w_1,\dots,w_{n-1}$.

The cycles we use for the lower bound are described in the following way.
We let $S$ be the set of sequences of $k$ integers in $[0,n)$ such that $\sum_{\ell = 1}^k s_\ell = \frac{n-1}{k-1}$,
where we use the notation $(s_1, s_2, \dots, s_k)$ for an element~$s \in S$.
A tuple of $k-1$ sequences in $S$ induces a graph $G$.
Let $(s^{(0)}, \dots, s^{(k-2)}) \in S^{k-1}$, the induced graph is partitioned into $k$ parts.
In the $i$\textsuperscript{th} part the weight $n^j$ is used exactly $s^{(j)}_i$ many times. See Figure~\ref{fig:construction}.

\begin{figure}[ht]
\centering
\includegraphics[width=.7\linewidth]{Fig/construction.eps}
\caption{Construction of the graph $G$ from the sequences $(s^{(0)}, \dots, s^{(k-2)}) \in S^{k-1}$. In this example, the $i$\textsuperscript{th} box is induced by the $i$\textsuperscript{th} sequence $s^{(i)}$ given by $s_0^{(i)} = 0, s^{(i)}_1 = 2, s^{(i)}_2 = 1, s^{(i)}_3 = 1, s^{(i)}_4 = 0$, and $s^{(i)}_5 = 1$.}
\label{fig:construction}
\end{figure}

The vertex in $G$ marking the end of the first box is $u_1 = \sum_{j = 0}^{k-2} s_1^{(j)} n^j$,
and more generally the vertex marking the end of the $i$\textsuperscript{th} box is 
\[
u_i = \sum_{j = 0}^{k-2} \left( \sum_{\ell = 1}^i s_\ell^{(j)} \right) n^j.
\]
Note that $\sum_{\ell = 1}^i s_\ell^{(j)}$ is the $j$\textsuperscript{th} digit of the number $u_i$ in base $n$,
since it belongs to $[0,\frac{n-1}{k-1}]$, and so it is $<n$.
Hence, $u_1,\dots,u_{k-1}$ fully determines the sequences $(s^{(0)}, \dots, s^{(k-2)})$.
We also let $u_0 = 0$.


Let $\phi : G \to \mathcal U$ be a homomorphism.
We define a function $f : S^{k-1} \to \mathcal U^k$ by
$f(s^{(0)}, \dots, s^{(k-2)}) = \left( \phi \left( u_i \right) : i \in [0,k) \right)$, which we prove to be injective.
The constraint on the sums of sequences on $S$ ensures that indeed the graph $G$ is a cycle of total weight~$0$, and then
thanks to Lemma~\ref{fact:equality} applied to the cycle $G$, we have
\[
\begin{array}{lll}
\phi(u_1) - \phi(u_0) & = & u_1 \\
\phi(u_2) - \phi(u_1) & = & u_2 \\
& \ \vdots & \\
\phi(u_{k-1}) - \phi(u_{k-2}) & = & u_{k-1},
\end{array}
\]
and as explained above the numbers $u_1,\dots,u_{k-1}$ fully determine the sequences $(s^{(0)}, \dots, s^{(k-2)})$.

Injectivity of $f$ implies that $|S|^{k-1} \le |\mathcal U|^k$.
The size of $S$ is 
\[
|S| = \binom{\frac{n-1}{k-1} + k-1}{k-1}
\ge \left( \frac{\frac{n-1}{k-1} + k-1}{k-1} \right)^{k-1} 
\ge \left( \frac{n-1}{(k-1)^2} \right)^{k-1},
\]
which implies (for $k$ constant)
$|\mathcal U| \geq \Omega \left( n^{ \frac{(k-1)^2}{k} } \right) = \Omega \left( n^{k-2} \right)$.
\end{proof}

\subsection{The complexity of solving mean payoff games using universal graphs}
\label{subsec:complexity_mean_payoff}

There is a very large literature on mean payoff games, a model independently introduced 
by Ehrenfeucht and Mycielski~\cite{EhrenfeuchtMycielski79} and by Gurvich, Karzanov, and Khachiyan~\cite{GKK88}
and studied in different research communities including program verification and optimisation.
The seminal paper of Zwick and Paterson~\cite{ZwickPaterson96} relates mean payoff games to discounted payoff games
and simple stochastic games, and most relevant to our work, constructs an algorithm for solving mean payoff games with complexity $O(n^2 m N)$,
where $n$ is the number of vertices, $m$ the number of edges, and $N$ the largest weight in absolute value.
If the weights are given in unary $N$ is polynomial in the representation, so we say that the algorithm is pseudo-polynomial.
The question whether there exists a polynomial time algorithm for mean payoff games with the usual representation of weights, meaning in binary,
is open.
The currently fastest algorithm for mean payoff games is randomised and achieves subexponential complexity $2^{\tilde{O}(\sqrt{n})}$.
It is based on randomised pivoting rules for the simplex algorithm devised by Kalai~\cite{Kalai92,Kalai97} and Matou\v{s}ek, Sharir and Welzl~\cite{MSW96}.

We are in this work interested in deterministic algorithms for solving mean payoff games.
Up until recently there were two fastest deterministic algorithms: the value iteration algorithm of Brim, Chaloupka, Doyen, Gentilini, and Raskin~\cite{BCDGR11}, which has complexity $O(n m N)$, and the algorithm of Lifshits and Pavlov~\cite{LP07} with complexity $O(n m 2^n)$.
They are incomparable: the former is better when $N \le 2^n$ and otherwise the latter prevails.
Recently Dorfman, Kaplan, and Zwick~\cite{DKZ19} presented an improved version of the value iteration algorithm
with a complexity $O(\min (n m N, n m 2^{n/2}))$, an improvement over the previous two algorithms when $N = \Omega(n 2^{n/2})$.

Solving a mean payoff game is very related to constructing an optimal strategy, meaning one achieving the highest possible value.
The state of the art for this problem is due to Comin and Rizzi~\cite{CominRizzi17} who designed a pseudo-polynomial time algorithm.

\vskip1em
Let us now construct algorithms from universal graphs combining Theorem~\ref{thm:MP_bounds_abs} and Theorem~\ref{thm:MP_bounds_card} with Theorem~\ref{thm:solving_product_game_linear}.

\begin{cor}
Let $n, N \in \mathbb N$.
The following statements use the RAM model with word size $w = \log(n) + \log(N)$.
\begin{itemize}
	\item There exists an algorithm for solving mean payoff games with weights in $[-N,N]$ of time complexity $O(nmN)$ and space complexity $O(n)$.
	\item There exists an algorithm for solving mean payoff games with weights in $[-N,N]$ of time complexity 
	$O(mn (nN)^{1 - 1/n})$ and with space complexity $O(n)$.
	\item There exists an algorithm for solving mean payoff games with $k$ weights of time complexity $O(m n^k)$ and space complexity $O(n)$.
\end{itemize}
\end{cor} 

The first algorithm is exactly the algorithm constructed by Brim, Chaloupka, Doyen, Gentilini, and Raskin~\cite{BCDGR11}: identical data structures and complexity analysis. 
The two tasks for manipulating universal graphs, 
namely computing $\delta(q,w)$ and checking whether $q \le q'$ 
are indeed unitary operations as they manipulate numbers of order $nN$.

Let us now discuss the significance of the difference between $N$ to $N^{1 - 1/n}$,
meaning the first and second algorithms.
Since $n$ is polynomial in the size of the input, one may say that $n$ is ``small'', 
while $N$ is exponential in the size of the input when weights are given in binary, hence ``large''.
For $N \le 2^n$ we have $N^{1 - 1/n} \ge \frac{1}{2} N$ so $N^{1 - 1/n}$ is essentially linear in $N$.
However when $N \ge 2^{\Omega(n^{1 + \varepsilon})}$ for $\varepsilon > 0$ then $2n^2 N^{1 - 1/n} = o(nN)$, 
so the second algorithm is indeed asymptotically faster.
To appreciate the relevance of this condition, let us recall an old result of Frank and Tardos~\cite{FT87} which implies that one can in polynomial time transform a mean payoff game into an equivalent one where $N \le 2^{4n^3} m^{m + 3}$.
Our new algorithm improves over the previous one for the range $N \in [2^{\Omega(n^{1 + \varepsilon})}, 2^{4n^3} m^{m + 3}]$.
We note however that the recent algorithm~\cite{DKZ19} (building over~\cite{BCDGR11} and \cite{GKK88}) is always faster than the second algorithm.

\vskip1em
As for the case of parity games, the lower bounds presented in Theorem~\ref{thm:MP_bounds_abs} and Theorem~\ref{thm:MP_bounds_card} show that to obtain faster algorithms we need to go beyond algorithms
based on universal graphs.
In particular there are no quasipolynomial universal graphs for mean payoff objectives, 
and the question whether the quasipolynomial time algorithms for parity games can be extended to mean payoff games
remains open.



\subsection{A universal graph of exponential size}

Let us fix a non-negative integer $n$.
We give a first construction of a $(n,\mathtt{Parity}(d))$-universal graph $\mathcal U$.
Its set of vertices is given by
\[
V(\mathcal U) = [0,n-1]^{d/2},
\]
that is, tuples of $d/2$ non-negative integers smaller than $n$.
Such tuples represent occurrences of odd priorities and for convenience we index with them using odd integers, and in a decreasing fashion, that is, $v \in V(\mathcal U)$ is denoted $v=(v_{d-1},v_{d-3}, \dots, v_3, v_1)$.

Following~\cite{J00}, we define an increasing sequence of total preorders 
\[
\leq_1 \subseteq \leq_3 \subseteq \dots \subseteq \leq_{d-1} \subseteq \leq_{d+1}
\]
over $V(\mathcal U)$, which are obtained by restricting to the first few values, and comparing lexicographically:
\[
v \leq_p v' \iff (v_{d-1}, v_{d-3}, \dots, v_p) \leq_{\mathrm{lex}} (v'_{d-1}, v'_{d-3}, \dots, v'_p).
\]
We use $v =_p v'$ to denote the equivalence relation induced by $\leq_p$, that is $v \leq_p v'$ and $v' \leq_p v$.
We write $v <_p v'$ if $\neg(v' \leq_p v)$.
Note that $\leq_{d+1}$ is the full relation: for all $v,v'$ we have $v =_{d+1} v'$.
At the other end of the scope, $\leq_1$ is antisymmetric, or in other words its equivalence classes are trivial and $=_1$ coincides with the equality.

The set of edges of $\mathcal U$ is given by
\[
(v,p,v') \in E(\mathcal U) \iff \begin{cases}
v >_p v' $ if $p$ is odd,$\\
v \geq_{p+1} v' $ if $p$ is even.$
\end{cases}
\]

Note that this condition is vacuous for $p=d$, every pair of vertices is connected (in both directions) by a $d$-edge.

\begin{lem}
\label{lem:first_construction_for_parity}
The graph $\mathcal U$ is $(n, \mathtt{Parity}(d))$-universal.
\end{lem}

\begin{proof}
We first show that $\mathcal U$ satisfies $\mathtt{Parity}(d)$.
Let $\pi=v_0 p_0 v_1 p_1 \dots$ be an infinite path in $\mathcal U$, and assume for contradiction that $p = \limsup_i p_i$ is odd: for all $i$ we have $p_i \leq p$, and for infinitely many $i$, $p_i = p$.
Then for all $i$ we have $(v_{i,d-1}, v_{i,d-3}, \dots v_{i,p}) \geq_\mathrm{lex} (v_{i+1,d-1}, v_{i+1,d-3}, \dots, v_{i+1,p})$ and this inequality is strict for infinitely many $i$'s, a contradiction.

We now show that $\mathcal U$ embeds all graphs of size $\leq n$ which satisfy $\mathtt{Parity}(d)$.
Let $G$ be such a graph.
Let $v \in G$, let $\pi=v_0 p_0 v_1 p_1 \dots$ be a path from $v$ in $G$, and let $p$ be an odd priority.
Consider the number $\mathrm{occ}_{\pi,p}$ of occurrences of $p$ in $\pi$ before a priority greater than $p$ is seen.
We claim that $\mathrm{occ}_{\pi,p} < n$, by a pumping argument.
Assume for contradiction that $\mathrm{occ}_{\pi,p} \geq n$, and let $i_1, \dots i_n$ denote the first $n$ occurrences of $p$ in $\pi$.
We have $p_{i_1} = \dots = p_{i_n} = p$, and for all $i \leq i_n$, $p_i \leq p$.
Then the $n+1$ vertices $v_{0},v_{i_1+1},v_{i_2+1}, \dots, v_{i_n+1}$ in this order, all have a path with maximal priority $p$ to the next one.
Since $G$ has $n$ vertices, there must be a repetition in this sequence, which induces an odd cycle.
Given a path $\pi$, we let $\mathrm{occ}_\pi = (\mathrm{occ}_{\pi,d-1}, \mathrm{occ}_{\pi, d-3}, \dots, \mathrm{occ}_{\pi,1})$.

We now define $\phi : V \to V(\mathcal U)$ by $\phi(v) = \max_\pi \mathrm{occ}_\pi$, where the max is taken lexicographically over all paths starting in $v$.
We claim that $\phi$ defines a graph homomorphism.
Let $e=(v,p,v')$ be an edge in $G$ and let $\pi'$ be a path from $v'$ in $G$ with maximal $\mathrm{occ}$.
Then $\pi = v p \pi'$ is a path from $v$ in $G$, satisfying $\mathrm{occ}_{\pi, p} = \mathrm{occ}_{\pi', p} + 1$ if $p$ is odd, and for all odd $\ell > p$, $\mathrm{occ}_{\pi, \ell} = \mathrm{occ}_{\pi', \ell}$.
If $p$ is odd this implies $\mathrm{occ}_{\pi} >_p \mathrm{occ}_{\pi'} = \phi(v')$, and if $p$ is even we have $\mathrm{occ}_{\pi} \geq_{p+1} \mathrm{occ}_{\pi'} = \phi(v')$.
In both cases, this yields $\phi(e) \in E(\mathcal U)$ since $\phi(v) \geq_\mathrm{lex} \mathrm{occ}_{\pi}$.
\end{proof}

The set $[0,n-1]^{d/2}$ of vertices of $\mathcal U$ can be seen as the set of leaves of the (ordered) complete tree of height $d/2+1$ and of degree $n$.
In this point of view, the equivalence relations $=_{2k+1}$ groups together leaves which belong to the same subtree at level $k$ (where by convention, the leaves are at level 0), hence the equivalence classes correspond to node of level $k$, which are naturally ordered left-to-right by $\leq_{2k+1}$.
In other words, a sequence of preorders $\leq_1 \subseteq \leq_3 \subseteq \dots \subseteq \leq_{d+1}$ over some set $V$ naturally induces a tree structure of height $d/2+1$ with leaves $V$.

It is not hard to see that $\mathcal U$ is saturated for the parity objective: the addition of any edge induces an odd cycle.
We will actually prove that every saturated graph is given by such a sequence of preorders, which induces the structure of a tree.
This will allow us to reformulate the universality condition over parity graphs as a universality condition over trees.


\subsection{Trees, tree-like graphs, and saturated parity graphs}
\label{subsec:saturated_graphs_parity}


Towards describing the structure of saturated graphs for the parity objective, we now define (ordered, levelled) trees.

A tree of height $h \geq 0$ is a finite subset $T$ of $\mathbb Z^h$.

As previously, we think of elements of a tree as representing occurrences of odd priorities. In this regard it is convenient to use odd numbers as indices, and we shall write $v=(v_{d-1}, v_{d-3}, \dots, v_{3}, v_1) \in T$, where $d=2h$.

A tree of height $h$ naturally defines an increasing sequence of $h+1$ total preorders
\[
\leq_1 \subseteq \leq_3 \subseteq \dots \subseteq \leq_{d-1} \subseteq \leq_{d+1},
\]
given by
\[
(v_{d-1}, v_{d-3}, \dots, v_{1}) \leq_p (v'_{d-1}, v'_{d-3}, \dots, v'_{1}) \iff (v_{d-1}, \dots, v_p) \leq_{\mathrm{lex}} (v'_{d-1}, v'_{d-3}, \dots, v'_p).
\]
Again, we use the standard notations relative to total preorders, $=_p$ denotes the equivalence relation associated with $\leq_p$, whose equivalence classes are stricly ordered by $<_p$.

\begin{figure}[ht]
\centering
\includegraphics[width=.22\linewidth]{Fig/tree2.eps}
\caption{The tree $T=\{000, 010, 011, 100, 111\}=\{u,v,w,x,y\}$. It has height $h=3$. We have $u =_5 v =_5 w <_5 x =_5 y$, and $u <_3 v =_3 w <_3 x <_3 y$.}
\label{fig:example_tree}
\end{figure}

Note that $\leq_{d+1}$ is the full relation, it has one equivalence class.
The order $\leq_1$ is antisymmetric; it is a total order, which coincides with $\leq_\mathrm{lex}$, and $=_1$ coincides with the equality over $T$.
Note that there is a unique tree of height $0$ which we call the empty tree, and that trees of height $1$ are sets of integers.

A tree $T$ of height $h$ induces a $[0,d]$-graph $\texttt{G}(T)$ with vertices $T$ defined as follows:
\begin{itemize}
\item for even $p$, $(v,p,v') \in E$ if and only if $v \geq_{p+1}^T v'$, and
\item for odd $p$, $(v,p,v') \in E$ if and only if $v >_{p}^T v'$.
\end{itemize}

\begin{figure}[ht]
\centering
\includegraphics[width=.6\linewidth]{Fig/tree_to_graph.eps}
\caption{On the left the tree $T=\{00,10,11\} = \{u,v,w\}$ and on the right, the graph $\texttt{G}(T)$.}
\label{fig:example_graph_to_tree}
\end{figure}

We say that graphs of the form $\texttt{G}(T)$, where $T$ is a tree, are tree-like.

\begin{lem}
\label{lem:trees_satisfy_parity}
Let $d \in \mathbb N$ be an even number and $T$ a tree of height $d/2$, then the graph $\texttt{G}(T)$ satisfies $\mathtt{Parity}(d)$, and moreover, it is saturated.
\end{lem}

\begin{proof}
We first show that $\texttt{G}(T)$ satisfies $\mathtt{Parity}(d)$, which is a direct adaptation of the first part of the proof of Lemma~\ref{lem:first_construction_for_parity}. We spell it out for completeness.
Let $\pi=v_0 p_0 v_1 p_1 \dots$ be an infinite path in $\texttt{G}(T)$, and assume for contradiction that $p = \limsup_i p_i$ is odd: for all $i$ we have $p_i \leq p$, and for infinitely many $i$, $p_i = p$.
Then for all $i$ we have $(v_{i,d-1}, v_{i,d-3}, \dots v_{i,p}) \geq_\mathrm{lex} (v_{i+1,d-1}, v_{i+1,d-3}, \dots, v_{i+1,p})$ and this inequality is strict for infinitely many $i$'s, a contradiction.

We now show that adding any edge to $\texttt{G}(T)$ yields a graph not satisfying $\mathtt{Parity}(d)$.
Let $e = (v,p,v')$ be an edge that does not appear in $\texttt{G}(T)$. 
If $p$ is even, then $v' >_{p+1} v$, 
so the edge $(v',p+1,v)$ belongs to $\texttt{G}(T)$, hence $\texttt{G}(T)_e$ contains an odd cycle. 
If $p$ is odd, then $v' \geq_{p} v$, which implies that the edge $(v',p-1,v)$ belongs to $\texttt{G}(T)$, 
and again $\texttt{G}(T)_e$ contains an odd cycle. 
\end{proof}

Now the second part of the proof of Lemma~\ref{lem:first_construction_for_parity} can be re-interpreted as follows.

\begin{lem}
\label{lem:universality_of_treelike}
Let $G$ be a graph satisfying $\mathtt{Parity}(d)$, where $d$ is even. There exists a tree $T$ of height $d/2$ and size $\leq |V|$ such that $G$ embeds in $\texttt{G}(T)$.
\end{lem}

\begin{proof}
We precisely mimic the proof of Lemma~\ref{lem:first_construction_for_parity}.
Given a path $\pi$ in $G$ and an odd priority $p \in \{1,3, \dots, d-1\}$, we again define $\mathrm{occ}_{\pi,p}$ to be the number of occurrences of $p$ in $\pi$ before a priority greater than $p$ is seen, and we let $\mathrm{occ}_{\pi}=(\mathrm{occ}_{\pi,d_1}, \mathrm{occ}_{\pi,d-3}, \dots, \mathrm{occ}_{\pi,1})$.
It is clear, since $G$ satisfies $\mathtt{Parity}(d)$, that all $\mathrm{occ}_{\pi,p}$'s are finite.
For $v \in V$, we define $\phi(v)$ to be the lexicographic maximum of $\mathrm{occ}_\pi$'s over paths $\pi$ starting in $v$, and put $T = \phi(V)$.


We prove that $\phi$ defines a homomorphism from $G$ to $\texttt{G}(T)$.
Let $e=(v,p,v')$ be an edge in $G$ and let $\pi'$ be a path from $v'$ in $G$ with maximal $\mathrm{occ}$.
Then $\pi = v p \pi'$ is a path from $v$ in $G$, satisfying $\mathrm{occ}_{\pi, p} = \mathrm{occ}_{\pi', p} + 1$ if $p$ is odd, and for all odd $\ell > p$, $\mathrm{occ}_{\pi, \ell} = \mathrm{occ}_{\pi', \ell}$.
If $p$ is odd this implies $\mathrm{occ}_{\pi} >_p \mathrm{occ}_{\pi'} = \phi(v')$, and if $p$ is even we have $\mathrm{occ}_{\pi} \geq_{p+1} \mathrm{occ}_{\pi'} = \phi(v')$.
In both cases, this yields $\phi(e) \in E(\mathcal U)$ since $\phi(v) \geq_\mathrm{lex} \mathrm{occ}_{\pi}$.
\end{proof}


Actually, it can be shown that, modulo contracting equivalence classes of $0$-edges which have the same ingoing and outgoing edges, saturated graphs are exactly tree-like graphs.
This is non-essential for what follows, but we prove it as an interesting side remark.

\begin{lem}
\label{lem:saturated_graphs_treelike}
Let $G$ be a saturated graph with respect to $\mathtt{Parity}(d)$, where $d$ is even, and such that for all $v,v'$, if both $(v,0,v')$ and $(v',0,v)$ are edges in $G$ then $v=v'$.
Then there exists a tree $T$ of height $d/2$ such that $G = \texttt{G}(T)$ up to renaming the vertices.
\end{lem}

\begin{proof}
By Lemma~\ref{lem:universality_of_treelike}, there exist $T$ of height $d/2$ and size $\leq |V|$ and a homomorphism $\phi$ from $G$ to $\texttt{G}(T)$.
It suffices to prove that $\phi$ is injective.
This ensures that the sets of vertices of $G$ and $\texttt{G}(T)$ are in bijection.
The inclusion $\phi(E) \subseteq E(\texttt{G}(T))$ follows simply from the fact that $\phi$ is a homomorphism, and the converse inclusion from the fact that $G$ is saturated.

Let $v,v' \in V$ be such that $\phi(v)=\phi(v')$.
We show that $e=(v,0,v')$ and $e'=(v',0,v)$ belong to $E$, which implies that $v=v'$.	
Assume $e$ and $e'$ do not both belong to $E$.
Since $G$ is saturated, there exists an infinite path $\pi=v_0 p_0 v_1 p_1 \dots$ in $G_{e,e'}$ with $\limsup_i p_i$ odd.
But by definition of $\texttt{G}(T)$, its vertices, and in particular $\phi(v)$, have $0$-self-loops, which implies that $\phi(e)=\phi(e')$ are edges in $\texttt{G}(T)$.
Hence, $\phi(\pi)= \phi(v_0) p_0 \phi(v_1) p_1 \dots$ is a path in $\texttt{G}(T)$ with odd limsup, a contradiction.
\end{proof}


Interpreting saturated graphs as trees allows us to rephrase the universal property for graphs as a simpler one for trees.

We say that a map $\phi: T \to T'$ where $T$ and $T'$ are trees of height $h$ is a tree-homomorphism if it preserves all orderings, that is, for all $v,v' \in T$, and for all odd $p$, 
\[
v \leq^T_p v' \iff \phi(v) \leq^{T'}_p \phi(v').
\]
An example is depicted in Figure~\ref{fig:example_embedding}.

\begin{lem}
\label{lem:equivalence_homomorphisms}
Let $T$ and $T'$ be two trees of height $d/2$, and let $\phi:T \to T'$.
Then $\phi$ is a tree-homomorphism if and only if it is a graph homomorphism from $\texttt{G}(T)$ to $\texttt{G}(T')$.
\end{lem}

\begin{proof}
Recall that $v <_p v'$ is the negation of $v \geq_p v'$. Hence we have
\[
\begin{array}{ccl}
& & \phi $ is a tree-homomorphism $ \\
& \iff & \forall v,v' \in V, \forall p$ odd, $ (v \leq^T_p v' \iff \phi(v) \leq_p^{T'} \phi(v')) \\[\medskipamount]

& \iff & \forall v,v' \in V
\left\{ \!
\begin{array}{cl}
\forall p $ even, $& (v \leq_{p+1}^{T} v' \implies \phi(v) \leq_{p+1}^T \phi(v')) \\
\forall p $ odd, $& (v <_p^{T} v' \implies \phi(v) <_{p}^{T} \phi(v'))
\end{array}
\right.\\[\bigskipamount]

& \iff & \forall v,v' \in V, \forall p, ((v',p,v) \in E(\texttt{G}(T)) \implies (\phi(v'),p,\phi(v') \in E(\texttt{G}(T')))\\[\medskipamount]
& \iff & \phi$ is a graph homomorphism.$
\end{array}
\]
\end{proof}

Thanks to Lemma~\ref{lem:universality_of_treelike} and~\ref{lem:equivalence_homomorphisms}, we may now shift our attention only to trees and their homomorphisms.
We say that a tree is $(n,h)$-universal if it has height $h$ and embeds all trees of height $h$ and size $\leq n$.

\begin{figure}[!ht]
\begin{center}
\includegraphics[width=.7\linewidth]{Fig/tree_embedding.eps}
\end{center}
\caption{On the left, a tree of height $2$ and size $11$.
This tree is $(5,2)$-universal, and is actually of minimal size.
On the right, a tree of size $5$ and one possible embedding in the universal tree.}
  \label{fig:example_embedding}
\end{figure}

\begin{lem}
The smallest $(n,h)$-universal trees and the smallest $(n, \mathtt{Parity} {2h})$-universal graphs have the same size.
\end{lem}

\begin{proof}
Let $G$ be a $(n, \mathtt{Parity}{2h}$-universal graph. By Lemma~\ref{lem:universality_of_treelike}, there is a tree $T$ of height $h$ not larger than $G$ and such that $G$ embeds into $\texttt{G}(T)$.
Let $T'$ be a tree of height $h$ and size $n$.
By universality of $G$, there is a homomorphism from $\texttt{G}(T')$ to $G$, which by composition induces a homomorphism from $\texttt{G}(T')$ to $\texttt{G}(T)$.
We conclude by Lemma~\ref{lem:equivalence_homomorphisms} that $T$ embeds $T'$, and hence $T$ is $(n,h)$-universal.

Conversely, let $T$ be $(n,h)$-universal, and let $G'$ be a graph satisfying $\mathtt{Parity}{2h}$.
By Lemma~\ref{lem:universality_of_treelike} there is a tree $T'$ of height $h$ such that $G'$ maps into $\texttt{G}(T')$.
Now $T'$ maps into $T$ by universality, by Lemma~\ref{lem:equivalence_homomorphisms}, this translates into a map from $\texttt{G}(T')$ to $\texttt{G}(T)$, and finally by composition on the left, $G'$ maps into $\texttt{G}(T)$.
We conclude that $\texttt{G}(T)$ is $(n,\mathtt{Parity}{2h})$-universal, and it has the same size as $T$.
\end{proof}

\subsection{Upper and lower bounds on universal trees}

We now study the size of the smallest $(n,h)$-universal trees.
In this subsection, we simply index elements of trees of height $h$ with integers from $h$ to $1$ for clarity.

\begin{thm}
\label{thm:universal_trees}
Let $n, h \in \mathbb N$.
\begin{itemize}
	\item There exists a $(n,h)$-universal tree of size at most 
	\[
	2n \cdot \binom{\lceil \log(n) \rceil + h - 1}{\lceil \log(n) \rceil},
	\]
	\item All $(n,h)$-universal trees have size at least 
	\[
	\binom{\lfloor \log(n) \rfloor + h - 1}{\lfloor \log(n) \rfloor}.
	\]
\end{itemize}
\end{thm}

Let us start with the upper bound.

\begin{prop}
\label{prop:upper_bounds_universal_tree}
There exists a $(n,h)$-universal tree with size $f(n,h)$, where $f$ satisfies the following recursion
\[
\begin{array}{lll}
f(n,h) & = & f(n,h-1) + f(\lfloor n/2 \rfloor,h) + f(n - 1 - \lfloor n/2 \rfloor,h), \\
f(n,1) & = & n, \\
f(1,h) & = & 1.
\end{array}
\]
\end{prop}

We refer to Appendix~\ref{sec:analysis_F} for an analysis of this recurrence, leading to the upper bound stated
in Theorem~\ref{thm:universal_trees}.
We further analyse this function when presenting the induced algorithm in Subsection~\ref{subsec:complexity_parity}.

\begin{proof}
We construct a $(n,h)$-universal tree $T$ by induction over $(n,h)$, lexicographically.
Trees of height $1$ and size $\leq n$ are (downward-closed) subsets of $[0, n-1]$, hence $[0,n-1]$ is $(n,1)$-universal.
There is a unique tree of size $1$ and height $h$, namely, $\{0^h\}$, and it is $(1,h)$-universal.
Now, let $n$ and $h$ be $>1$ and assume constructed $(n',h')$-universal trees of size $f(n',h')$ for each $(n',h') <_\mathrm{lex} (n,h)$.
Let
\begin{itemize}
	\item $T_\mathrm{left}$ be a $(\lfloor n/2 \rfloor,h)$-universal tree,
	\item $T_\mathrm{middle}$ be a $(n,h-1)$-universal tree, and
	\item $T_\mathrm{right}$ be a $(\lceil n/2 \rceil - 1,h)$-universal tree.
\end{itemize}
Intuitively, we construct $T$ by merging the roots of $T_\mathrm{left}$ and of $T_\mathrm{right}$ and inserting in between a child of the root to which $T_\mathrm{middle}$ is attached.

\begin{figure}[!h]
\centering
\includegraphics[scale=.56]{Fig/smallest_tree_construction.eps}
\caption{The inductive construction.}
\label{fig:smallest_tree_construction}
\end{figure}

Formally, we let $\ell = \max_{v \in T_\mathrm{left}} v_{h}$ be the number of children of $T_\mathrm{left}$, and put
\[
T = T_\mathrm{left} \cup \ell \cdot T_\mathrm{middle} \cup (T_\mathrm{right} + (\ell +1, 0, \dots, 0)).
\] 

We now argue that $T$ is $(n,h)$-universal.
Consider a tree $T'$ of height $h$ and size $n$.
We let $p = \max_{v \in T'} v_{h}$ be the number of children of $T'$.
For each $i \in \{0, \dots, p\}$, let $n_i$ be the number of leaves in the $i$-th child of $T'$, that is, $n_i=\{v \in T' \mid v_{h} = i\}$.
Since $n_0 + n_1 + \dots + n_p = n$, there is $i_0$ such that $n_{0} + \dots + n_{i_0 -1} \leq \lfloor n/2 \rfloor$ and $n_{0} + \dots + n_{i_0-1} + n_{i_0} > \lfloor n/2 \rfloor$, which implies $n_{i_0 +1} + \dots + n_p \leq \lceil n/2 \rceil - 1$.

Consider the three trees $T'_\mathrm{left} = \{v \in T' \mid v_{h} < i_0\}$, $T'_\mathrm{middle} = \{(v_{h-1}, \dots, v_1) \in \mathbb N^{h-1} \mid (i_0,v_{h-1}, \dots, v-1) \in T'\}$ and $T'_\mathrm{right} = \{v \in T' \mid v_{d-1} > i_0\} - (i_0+1, 0, \dots, 0)$.

The trees $T'_\mathrm{left}$ and $T'_\mathrm{right}$ have height $h$ and respective sizes $\leq \lfloor n/2 \rfloor$ and $\leq \lceil n/2 \rceil - 1$, hence they map respectively, via $\phi_\mathrm{left}$ and $\phi_\mathrm{right}$ into $T_\mathrm{left}$ and $T_\mathrm{right}$. 
Likewise, the tree $T'_\mathrm{middle}$ has height $h-1$ and size at most $n$, hence it has a homomorphism $\phi_\mathrm{middle}$ into $T_\mathrm{middle}$.
These are combined into a map $\phi$ from $T'$ to $T$ by
\[
\phi(v) = \left\{ \! \begin{array}{ll}
\phi_\mathrm{left}(v) & $ if $ v_h < i_0 \\
i_0 \cdot \phi_\mathrm{middle}(v_{h-1}, \dots, v_1) & $ if $v_h = i_0 \\
(\ell +1, 0, \dots, 0) + \phi_{\mathrm{right}}(v - (i_0+1,0 \dots, 0)) & $ if $v_h > i_0. 
\end{array}
\right.
\]
We now prove that $\phi$ is indeed a tree-homomorphism from $T'$ to $T$. 
Let $k \in \{1, \dots, h\}$ and let $v,v' \in T'$.
If $v_h$ and $v'_h$ are either both $< i_0$, both $= i_0$, or both $> i_0$, then they both correspond to vertices of $T'_\mathrm{left}$ or of $T'_\mathrm{middle}$ or of $T'_\mathrm{right}$, and we conclude that $v \leq^{T'}_k v' \iff \phi(v) \leq^T_k \phi(v')$ by invoking the fact that either $\phi_\mathrm{left}, \phi_\mathrm{middle}$ or $\phi_\mathrm{right}$ is a tree-homomorphism.
Otherwise, without loss of generality $v \leq v'$, and we even have $v_h \leq i_0 \leq v'_h$ with one of these inequalities being strict, hence $v <^{T'}_k v'$, whatever the value of $k$.
By definition of $\phi$ we have $\phi(v)_h \leq \ell \leq \phi(v')_h$ with the same inequality being strict, which likewise implies that $\phi(v) <^T_k \phi(v')$, the wanted result.
Hence $T$ is universal, which concludes the proof.
\end{proof}

We now prove a lower bound on the size of universal trees.

\begin{prop}
Any $(n,h)$-universal tree has at size at least $g(n,h)$, where $g$ satisfies the following recursion
\[
\begin{array}{lll}
g(n,h) & = & \sum_{\delta = 1}^n g(\lfloor n / \delta \rfloor,h-1), \\
g(n,1) & = & n, \\
g(1,h) & = & 1.
\end{array}
\]
\end{prop}

We refer to Appendix~\ref{sec:analysis_G} for an analysis of this recurrence, leading to the lower bound stated
in Theorem~\ref{thm:universal_trees}.

The upper and lower bounds do not match perfectly.
However, 
\[
\frac{f(n,h)}{g(n,h)} \le 2^{\lceil \log(n) \rceil} \cdot \frac{\lfloor \log(n) \rfloor + h}{\lfloor \log(n) \rfloor} = O(n h),
\]
\textit{i.e.} they are polynomially related.

\begin{proof}
The bounds are clear for $h = 1$ or $n = 1$.
We let $h>1$ assumed the result known for $h-1$, and let $T$ be a $(n,h)$-universal tree, and we let $\delta \in [1,n]$. 
We construct a tree $T_\delta$ of height $h-1$ by restricting to subtrees of height 1 which have $\geq \delta$ children, that is
\[
T_\delta=\{v \in \mathbb N^{h-1} \mid |\{k \mid v \cdot k \in T\}| \geq \delta\},
\]
and argue that $T_\delta$ is $(\lfloor n / \delta \rfloor,h-1)$-universal.

\begin{figure}[ht]
\begin{center}
\includegraphics[width = 0.59 \linewidth]{Fig/parity_lower_bound_construction.eps}
\end{center}
\caption{In black the tree $T$ and its lowest level, and in red the tree $T_4$ obtained for $\delta=4$.}
\label{fig:parity_lower_bound_construction}
\end{figure}

Indeed, let $T'$ be a tree of height $h-1$ with $\lfloor n / \delta \rfloor$ leaves.
To each leaf of $T'$ we append $\delta$ children, that is, we consider
\[
T'' = T \times [0, \delta-1],
\]
which has size $\leq n$ and height $h$.
Since $T$ is $(n,h)$-universal, there is a tree-homomorphism $\phi$ from $T''$ to $T$.
Now, for each $v \in T'$, the elements $v \cdot 0, \dots, v \cdot (\delta -1)$ of $T''$ are different and $2$-equivalent in $T''$, hence so must be their image in $T$.
As a consequence, $\phi'(v)$ defined by $\phi'(v)=(\phi(v\cdot 0)_h, \dots, \phi(v\cdot (\delta -1)_{1})$ satisfies $|\{k \mid \phi'(v) \cdot k \in T\}| \geq k$, or in other words, $\phi'(v) \in T_\delta$, and $\phi'$ preserves all orders just because $\phi$ does.
Hence, $\phi'$ embeds $T$ in $T_\delta$, and we conclude that $T_\delta$ is $(\lfloor n / \delta \rfloor,h-1)$-universal.

In particular, the induction hypothesis tells us that $T_\delta$ has size at least $g(\lfloor n / \delta \rfloor,h-1)$.
Summing over values of $\delta$, we count each $2$-equivalent class of $T$ as many times as its size, which concludes with the wanted bound.
\end{proof}

\subsection{The complexity of solving parity games using universal graphs}
\label{subsec:complexity_parity}

Let us start with reviewing the recent results on parity games and their relationships with separating automata, GFSG automata, and universal trees.

The first quasipolynomial time algorithm comes in three flavours: the original version~\cite{CJKLS17}, as a value iteration algorithm~\cite{FJSSW17}, and as a separating automaton~\cite{BC18}.
The second quasipolynomial time algorithm called succinct progress measure lifting algorithm~\cite{JL17} is a value iteration algorithm; it was presented using the formalism of universal trees in~\cite{Fij18}, and then as a separating automaton in~\cite{CDFJLP18}.

Hence deterministic models (separating automata) are expressive enough to capture the first two algorithms; the situation changes with the register games algorithm~\cite{Leh18}. 
Indeed it was observed in~\cite{CDFJLP18} that the algorithm induces a `non-deterministic separating automaton', meaning an automaton $\mathcal{A}$ satisfying $\Omega^{|n} \subseteq L(\mathcal{A}) \subseteq \Omega$; this was enough to subject this third algorithm to the lower bound on the size of separating automata since the result of~\cite{CDFJLP18} applies to non-deterministic automata (in the same way as Theorem~\ref{thm:main} does).
However this is not enough to prove the correctness of the construction: under this assumption the two games $\mathcal{G}$
and $\mathcal{G} \triangleright \mathcal{A}$ may not be equivalent.
The follow-up paper~\cite{Parys20} investigated this issue and offered a sufficient condition for a non-deterministic separating automaton to ensure the equivalence between $\mathcal{G}$ and $\mathcal{G} \triangleright \mathcal{A}$.
This condition is almost the same as the good-for-small-games condition we introduced independently in~\cite{CF19},
the only differences are that in the framework of~\cite{Parys20} the automata read edges (meaning triples $(v,p,v')$) 
while here the automata only read priorities, and the good-for-small-games strategy depends on the graph.
The journal version of the register games algorithm suggested the name `good-for-small-games'~\cite{LehtinenB20}.

We further discuss in the conclusions section (Section~\ref{sec:conclusions}) the recent extensions of the register games algorithm.

\vskip1em
The main conclusion of our studies on universal graphs and trees is the following algorithm,
combining Theorem~\ref{thm:universal_trees} and Theorem~\ref{thm:solving_product_game_linear}.

\begin{cor}
Let $n, m, d \in \mathbb N$.
There exists an algorithm\footnote{In the RAM model with word size $w = \log(n) \cdot \log(d)$.} solving parity games with $n$ vertices, $m$ edges, and priorities in $[0,d]$ in time 
\[
O\left(m n \cdot \binom{\lceil \log(n) \rceil + d/2 - 1}{\lceil \log(n) \rceil}\right).
\]
\end{cor}

A generous upper bound on the expression above is $n^{O(\log(d))}$.
A refined calculation reveals that the expression is polynomial in $n$ and $d$ if $d = O(\log(n))$.
We refer to~\cite{JL17} for the tightest existing analysis of the binomial coefficient.

The choice of word size $w = \log(n) \cdot \log(d)$ is inherited from the generic value iteration algorithm using word 
size $\log(|V|) + \log(|Q|)$, because $|Q| = n^{O(\log(d))}$.
For this word size it is easy to verify that the two following operations on universal trees take constant time: 
computing $\delta(q,p)$ and comparing $q \le q'$.
Choosing the word size $w = \log(n)$ implies that a leaf of the universal tree 
cannot anymore be represented in a single machine word: 
the `succinct encoding' proposed in~\cite{JL17} performs the two operations above in a very low complexity (polylogarithmic in time) in this setting.

The complexity of (variants of) this algorithm has been investigated by Chatterjee, Dvor{\'a}k, Henzinger, and Svozil 
in the set-based symbolic model~\cite{CDHS18}, which is a different computational model; the differences are only in polynomial factors.

The second outcome of our analysis is a lower bound argument.

\begin{cor}{}
\label{cor:lower_bounds_parity}
All algorithms based on separating automata, GFSG automata, or universal graphs, have at least quasipolynomial complexity.
\end{cor}

This extends the main result of~\cite{CDFJLP18} which stated this result using non-deterministic separating automata and universal trees.
The statement is kept informal since its value is not in its exact formalisation but in the perspectives it offers:
all existing quasipolynomial time algorithms for parity games have been tightly related to the notion of universal trees.
Corollary~\ref{cor:lower_bounds_parity} states that to improve further the complexity of solving parity games one needs to go beyond the notion of universal trees.

\subsection{Graphs are safety automata and safety automata are graphs}

\paragraph*{Graphs}
We consider edge labelled directed graphs: 
a graph $G$ is given by a (finite) set $V$ of vertices and a (finite) set $E \subseteq Q \times C \times Q$ of edges,
with $C$ a set of colours, so we write $G = (V,E)$.
It is sometimes convenient to use $V(G)$ for $V$ and $E(G)$ for $E$, to avoid any ambiguity.
An edge $(v,c,v')$ is from the vertex $v$ to the vertex $v'$ and is labelled by the colour $c$.
The size of a graph is its number of vertices.
A vertex $v$ for which there exists no outgoing edges $(v,c,v') \in E$ is called a sink.

\paragraph*{Paths}
A path $\pi$ is a (finite or infinite) sequence 
\[
\pi = v_0 c_0 v_1 c_1 v_2 \dots
\]
where for all $i$ we have $(v_i,c_i,v_{i+1}) \in E$.
If it is finite, that is, $\pi= v_0 c_0 \dots c_{i-1} v_i$, we call $\text{len}(\pi) = i \geq 0$ the length of $\pi$, 
and use $\text{last}(\pi)$ to denote the last vertex $v_i$.
The length of an infinite path is $\infty$.
We say that $\pi$ starts from $v_0$ or is a path from $v_0$, 
and in the case where $\pi$ is finite we say that $\pi$ is a path ending in $\text{last}(\pi)$ or simply a path to $\text{last}(\pi)$.
We say that $v'$ is reachable from $v$ if there exists a path from $v$ to $v'$.
We let $\pi_{\le i}$ denote the prefix of $\pi$ ending in $v_i$, meaning 
$\pi_{\le i} = v_0 c_0 v_1 \dots c_{i-1} v_i$.
A cycle is a path from a vertex to itself of length at least one.

We use $\text{Path}_{\text{fin}}(G), \text{Path}_{\infty}(G)$ and $\text{Path}(G)$ to denote respectively the sets of finite paths of $G$, infinite paths of $G$, and their union. We sometimes drop $G$ when it is clear from context. 
For $v_0 \in V$ we also use $\text{Path}_{\text{fin}}(G,v_0), \text{Path}_{\infty}(G,v_0)$ and $\text{Path}(G,v_0)$ 
to refer to the sets of paths starting from $v_0$. 
We use $\text{col}(\pi)$ to denote the (finite or infinite) sequence of colours $c_0 c_1 \dots$ induced by $\pi$.

\paragraph*{Objectives}
An objective is a set $\Omega \subseteq C^\omega$ of infinite sequences of colours.
We say that a sequence of colours belonging to $\Omega$ satisfies $\Omega$, and extend this terminology to infinite paths $\pi$ with $\text{col}(\pi) \in \Omega$.

\begin{defi}[Graphs satisfying an objective]
Let $\Omega$ be an objective and $G$ a graph.
We say that $G$ satisfies $\Omega$ if all infinite paths in $G$ satisfy $\Omega$.
\end{defi}

\paragraph*{Safety automata}
A safety automaton over the alphabet $C$ is given by a finite set of states $Q$ and a transition function 
$\Delta \subseteq Q \times C \times Q$, so we write $\mathcal{A} = (Q,\Delta)$.
Since we are only considering safety automata in this paper, we omit the adjective safety and simply speak of an automaton.
A first very important remark is that a (safety) automaton is simply a graph; 
this point of view will be very important and fruitful in this paper.

An automaton $\mathcal{A}$ recognises the language $L(\mathcal{A})$ of infinite words defined as follows:
\[
L(\mathcal{A}) = \set{\text{col}(\pi) : \pi \text{ infinite path in } \mathcal{A}}.
\]
The class of deterministic automata has two additional properties: 
the automaton $\mathcal{A}$ has a designated initial state $q_0$, and for any state $q \in Q$ and colour $c \in C$ 
there is at most one transition of the form $(q,c,q')$ in $\Delta$.
In that case we define $\delta : Q \times C \to Q$ such that 
$\delta(q,c)$ is the unique $q'$ where $(q,c,q') \in \Delta$ if it is defined. 
We extend $\delta$ to sequences of colours by the formulas 
$\delta^*(q,\epsilon) = q$ and $\delta^*(q,wc) = \delta(\delta^*(q,w),c)$.
The language recognised by a deterministic automaton $\mathcal{A}$ is $L(\mathcal{A})$ defined by
$L(\mathcal{A}) = \set{\text{col}(\pi) : \pi \text{ infinite path from $q_0$}}$.
Note that if $w$ is a finite prefix of a word in $L(\mathcal{A})$, then $\delta^*(q_0,w)$ is well defined.

Following our convention to identify non-deterministic automata and graphs, we say that $\mathcal{A}$ satisfies $\Omega$ 
if $L(\mathcal{A}) \subseteq \Omega$.

\subsection{Games}

\paragraph*{Arenas}
An arena is given by a graph $G$ together with a partition $V = \text{V}_{\text{Eve}} \uplus \text{V}_{\text{Adam}}$ of its set of vertices describing which player controls each vertex.
We represent vertices controlled by Eve with circles and those controlled by Adam with squares.

\paragraph*{Games}
A game is given by an arena and an objective $\Omega$.
We often let $\mathcal{G}$ denote a game, its size is the size of the underlying graph.
It is played as follows.
A token is initially placed on some vertex $v_0$, and the player who controls this vertex pushes the token along an edge, 
reaching a new vertex; the player who controls this new vertex takes over, 
and this interaction goes on, either forever and describing an infinite path, or until reaching a sink.

We say that a path is winning\footnote{We always take the point of view of Eve, so winning means winning for Eve, and similarly a strategy is a strategy for Eve.} if it is infinite and satisfies $\Omega$, or finite and ends in a sink controlled by Adam.
The definition of a winning path includes the following usual convention: if a player cannot move they lose,
in other words sinks controlled by Adam are winning (for Eve) and sinks controlled by Eve are losing.

We extend the notations $\text{Path}_{\text{fin}}, \text{Path}_{\infty}$ and $\text{Path}$ to games by considering the underlying graph.

\paragraph*{Strategies}
A strategy in $\mathcal{G}$ is a partial map $\sigma : \text{Path}_{\text{fin}}(\mathcal{G}) \to E$ such that $\sigma(\pi)$ is 
an outgoing edge of $\text{last}(\pi)$ when it is defined.
We say that a path $\pi = v_0 c_0 v_1 \dots$ is consistent with $\sigma$ if
for all $i < \text{len}(\pi)$, if $v_i \in \text{V}_{\text{Eve}}$ then $\sigma$ is defined over $\pi_{\leq i}$ and 
$\sigma(\pi_{\le i}) = (v_i, c_i, v_{i+1})$.
A consistent path with $\sigma$ is maximal if it is not the strict prefix of a consistent path with $\sigma$
(in particular infinite consistent paths are maximal).

A strategy $\sigma$ is winning from $v_0$ if all maximal paths consistent with $\sigma$ are winning.
Note that in particular, if a finite path $\pi$ is consistent with a winning strategy $\sigma$ and ends in a vertex which belongs to Eve, then $\sigma$ is defined over $\pi$.
We say that $v_0$ is a winning vertex of $\mathcal{G}$ or that Eve wins from $v$ in $\mathcal{G}$ 
if there exists a winning strategy from $v_0$, and let $\text{W}_{\text{Eve}}(\mathcal{G})$ denote the set of winning vertices.

\paragraph*{Positional strategies}
Positional strategies make decisions only considering the current vertex. 
Such a strategy is given by $\widehat \sigma : \text{V}_{\text{Eve}} \to E$.
A positional strategy induces a strategy $\sigma : \text{Path}_{\text{fin}} \to E$ from any vertex $v_0$ 
by setting ${\sigma}(\pi) = \widehat{\sigma}(\text{last}(\pi))$ when $\text{last}(\pi) \in \text{V}_{\text{Eve}}$.

\begin{defi}[Positionally determined objectives]
We say that an objective $\Omega$ is \textit{positionally determined} if for every game with objective $\Omega$ and vertex $v_0$,
if $v_0 \in \text{W}_{\text{Eve}}(\mathcal{G})$ then there exists a positional winning strategy from $v_0$.
\end{defi}

Given a game $\mathcal{G}$, a vertex $v_0$, and a positional strategy $\sigma$ we let $\mathcal{G}[\sigma,v_0]$ denote the graph obtained by restricting $\mathcal{G}$ to vertices reachable from $v_0$ by playing $\sigma$ and to the moves prescribed by $\sigma$.
Formally, the set of vertices and edges is
\[
\begin{array}{lll}
V[\sigma,v_0] & = & \set{v \in V : \text{there exists a path from } v_0 \text{ to } v \text{ consistent with } \sigma}, \\
E[\sigma,v_0] & = & \set{(v,c,v') \in E : v \in \text{V}_{\text{Adam}} \text{ or } \left( v \in \text{V}_{\text{Eve}} \text{ and }\right.
\left. \sigma(v) = (v,c,v') \right)} \\
& \cap & V[\sigma,v_0] \times C \times V[\sigma,v_0].
\end{array}
\]

\begin{defi}[Prefix independent objectives]
We say that an objective $\Omega$ is prefix independent if for all $u \in C^*$ and $v \in C^\omega$, 
we have $uv \in \Omega$ if and only if $v \in \Omega$.
\end{defi}

\begin{fact}\label{fact:game_mp}
Let $\Omega$ be a prefix independent objective, $\mathcal{G}$ a game, $v_0$ a vertex, and $\sigma$ a positional strategy.
Then $\sigma$ is winning from $v_0$ if and only if the graph $\mathcal{G}[\sigma,v_0]$ satisfies $\Omega$
and does not contain any sink controlled by Eve.
\end{fact}

\paragraph*{Safety games}
The safety objective $\mathtt{Safe}$ is defined over the set of colours $C = \set{\varepsilon}$ by $\mathtt{Safe} = \set{\varepsilon^\omega}$: 
in words, all infinite paths are winning, so losing for Eve can only result from reaching a sink that she controls.
Since there is a unique colour, when manipulating safety games we ignore the colour component for edges.
Note that in safety games, strategies can equivalently be defined as maps to $V$ (and not $E$):
only the target of an edge matters when the source is fixed, since there is a unique colour.
We sometimes use this abuse of notations for the sake of simplicity and conciseness.

The following lemma is folklore, we refer to Section~\ref{sec:value_iteration} for more details on the algorithm.
The statement uses the classical RAM model with word size $w = \log(|V|)$.

\begin{thm}\label{thm:safety_games}
There exists an algorithm computing the set of winning vertices of a safety game running in time $O(|E|)$.
\end{thm}

\subsection{Assumptions on objectives}
\label{subsec:assumptions}

\begin{defi}[Neutral letter]
Let $\Omega \subseteq C^\omega$ an objective and $0 \in C$.
For $w \in C^\omega$ we let $\text{Proj}(w)$ denote the projection of $w$ on $C \setminus \set{0}$.
We say that $0$ is a \textit{neutral letter} if
for all $w \in C^\omega$, if $\text{Proj}(w)$ is finite then $w \in \Omega$, and if $\text{Proj}(w)$ is infinite,
then $w \in \Omega$ if and only if $\text{Proj}(w) \in \Omega$.
\end{defi}

In this paper, we will prove results applying to general objectives $\Omega$ satisfying three assumptions:
\begin{itemize}
	\item $\Omega$ is positionally determined,
	\item $\Omega$ is prefix independent,
	\item $\Omega$ has a neutral letter.
\end{itemize}
The first assumption is at the heart of the approach; the other two are here only for technical convenience.

\subsection{Product construction}
\label{subsec:product}

Let $\mathcal{A} = (Q, \Delta)$ be an automaton and $\mathcal{G}$ a game with objective $\Omega$.
We define the chained game $\mathcal{G} \triangleright \mathcal{A}$ as the safety game with vertices $V' = \text{V}_{\text{Eve}}' \uplus \text{V}_{\text{Adam}}'$ and edges $E'$ given by
\[
\begin{array}{lll}
\text{V}_{\text{Eve}}' & = & \text{V}_{\text{Eve}} \times Q \uplus E\times Q, \\
\text{V}_{\text{Adam}}' & = & \text{V}_{\text{Adam}} \times Q, \\
E' & = & \{((v,q), ((v,c,v'),q)) : q \in Q, (v,c,v') \in E\} \\
& \cup & \{(((v,c,v'),q), (v',q')) : (v,c,v') \in E, (q,c,q') \in \Delta\}.
\end{array}
\]

In words, from $(v,q) \in V \times Q$, the player whom $v$ belongs to chooses an edge $e=(v,c,v') \in E$, and the game progresses to $(e,q)$.
Then Eve chooses a transition $(q,c,q')$ in $\mathcal{A}$, and the game continues from $(v',q')$.
Intuitively, we simulate playing in $\mathcal{G}$, but additionally Eve has to simultaneously  follow a path in $\mathcal{A}$ which reads the same colours.
Note that the obtained game $\mathcal{G} \triangleright \mathcal{A}$ is a safety game: Eve wins if she can play forever or end up in a sink controlled by Adam.

\begin{lem}\label{lem:product_harder}
Let $\Omega$ be an objective, $\mathcal{G}$ a game with objective $\Omega$, $\mathcal{A}$ an automaton, and $v_0 \in V$.
If $\mathcal{A}$ satisfies $\Omega$ and $q_0 \in Q$ is such that Eve wins from $(v_0,q_0)$ in $\mathcal{G} \triangleright \mathcal{A}$, then Eve wins from $v_0$ in $\mathcal{G}$.
\end{lem}

Intuitively, if Eve can play forever in $\mathcal{G} \triangleright \mathcal{A}$, and all paths in $\mathcal{A}$ are labelled by sequences which belong to $\Omega$, then Eve can use the same strategy in $\mathcal{G}$ and obtain a path satisfying $\Omega$.
The formal proof requires some technical care for transferring the strategy from $\mathcal{G} \triangleright \mathcal{A}$ to $\mathcal{G}$.

\begin{proof}
Let $\sigma'$ be a winning strategy from $(v_0, q_0)$ in $\mathcal{G} \triangleright \mathcal{A}$.
We construct a strategy $\sigma$, from $v_0$ in $\mathcal{G}$ which simulates $\sigma'$ in the following sense,
which we call the simulation property:
\begin{center}
for any path $\pi = v_0 c_0 \dots c_{i-1} v_i$ in $\mathcal{G}$ which is consistent with $\sigma$, \\
there exists a sequence of states $q_0 \dots q_i$ such that $\pi' = (v_0, q_0)(e_0,q_0) \dots (v_i, q_i)$, \\
with $e_j = (v_j,c_j,v_{j+1})$ for $j < i$, is a path in $\mathcal{G} \triangleright \mathcal{A}$ consistent with $\sigma'$.
\end{center}

We define $\sigma$ over finite paths $v_0c_0 \dots c_{i-1}v_i$ with $v_i \in \text{V}_{\text{Eve}}$ by induction over $i$, so that the simulation property holds.
For $i=0$ there is nothing to prove since $\pi'=(v_0,q_0)$ is a path in $\mathcal{G} \triangleright \mathcal{A}$ consistent with $\sigma'$.
Let $\pi = v_0 c_0 \dots c_{i-1} v_{i}$ be a path in $\mathcal{G}$ consistent with $\sigma$ and $v_i \in \text{V}_{\text{Eve}}$, 
we want to define $\sigma(\pi)$.
Thanks to the simulation property there exists $q_0 \dots q_i$ such that 
$\pi' = (v_0, q_0)(e_0, q_0) \dots (v_{i}, q_{i})$ is a path in $\mathcal{G} \triangleright \mathcal{A}$ consistent with $\sigma'$.
Then $(v_i,q_i) \in \text{V}_{\text{Eve}}'$, so since it is winning, $\sigma'$ is defined over $\pi'$, let us write $\sigma'(\pi') = (e_i,q_i)$ with $e_i = (v_i,c_i,v_{i+1})$. 
We set $\sigma(\pi) = e_i$.

To conclude the definition of $\sigma$ we need to show that the simulation property extends to paths
of length $i+1$.
Let $\pi_{i+1} = \pi\ c_i v_{i+1} = v_0 c_0 \dots v_i c_i v_{i+1}$ be consistent with $\sigma$.
We apply the simulation property to $\pi$ to construct $q_0 \dots q_i$ such that
$\pi' = (v_0, q_0)(e_0, q_0) \dots (v_{i}, q_{i})$ is a path in $\mathcal{G} \triangleright \mathcal{A}$ consistent with $\sigma'$.
Let us consider $\pi'_{+1} = \pi'\ (e_i,q_i)$ with $e_i = (v_i,c_i,v_{i+1})$, we claim that $\pi'_{+1}$ is consistent with $\sigma'$.
Indeed, if $v_i \in \text{V}_{\text{Adam}}$, there is nothing to prove, and if $v_i \in \text{V}_{\text{Eve}}$, this holds by construction: 
since $\sigma(\pi) = e_i$ we have $\sigma'(\pi') = (e_i,q_i)$.
Now $(e_i,q_i) \in \text{V}_{\text{Eve}}$ so $\sigma'$ is defined over $\pi'_{+1}$, and we let $\sigma'(\pi'_{+1}) = (v_{i+1}, q_{i+1})$.
Then $\pi'_{+2} = \pi'_{+1} (v_{i+1}, q_{i+1})$ is consistent with $\sigma'$.
This concludes the inductive proof of the simulation property together with the definition of $\sigma$.

\vskip1em
We now prove that $\sigma$ is a winning strategy from $v_0$. 
Let $\pi=v_0 c_0 v_1 \dots$ be a maximal consistent path with $\sigma$, and let $\pi' = (v_0,q_0)(e_0,q_0)(v_1,q_1)(e_1,q_1) \dots$ be the corresponding path in $\mathcal{G} \triangleright \mathcal{A}$ consistent with $\sigma'$.
Let us first assume that $\pi$ is finite, and let $v_i = \text{last}(\pi)$. If $v_i \in \text{V}_{\text{Eve}}$, then by construction $\sigma$ is defined over $\pi$, so the path $v_0c_0 \dots v_i c_i v_{i+1}$, where $\sigma(\pi)=(v_i,c_i,v_{i+1})$ is consistent with $\sigma$, contradicting maximality of $\pi$. If however $v_i \in \text{V}_{\text{Adam}}$, then by maximality of $\sigma$, $v_i$ must be a sink, hence $\pi$ is winning.
Now if $\pi$ is infinite then so is $\pi'$, and then $q_0 c_0 q_1 c_1 \dots$ is a path in $\mathcal{A}$, so $\text{col}(\pi) = c_0 c_1 \dots \in L(\mathcal{A}) \subseteq \Omega$, and $\pi$ is winning.
We conclude that $\sigma$ is a winning strategy from $v_0$ in $\mathcal{G}$.
\end{proof}


Hence, assuming that $\mathcal{A}$ satisfies $\Omega$, winning $\mathcal{G}$ is always easier for Eve than winning $\mathcal{G} \triangleright \mathcal{A}$. The three following sections introduce three different settings where the converse holds, that is, $\mathcal{G}$ and $\mathcal{G} \triangleright \mathcal{A}$ are equivalent. In particular, via Theorem~\ref{thm:safety_games}, this leads to algorithms with runtime $O(|E'|)$ 
which is bounded by $O(|E| \cdot |\Delta|)$ for computing the winning region in $\mathcal{G}$.

\subsection{Separating automata}
\label{subsec:separating}
It is not hard to see that if $\mathcal{A}$ is deterministic and recognises exactly $\Omega$, then $\mathcal{G}$ and $\mathcal{G} \triangleright \mathcal{A}$ are equivalent.
However, for many objectives $\Omega$ (for instance, parity or mean payoff objectives), a simple topological argument shows that such deterministic automata do not exist.
Separating automata are defined by introducing $n$ as a parameter, and relaxing the condition $L(\mathcal{A})=\Omega$ to the weaker condition $\Omega^{\mid n} \subseteq L(\mathcal{A}) \subseteq \Omega$, where $\Omega^{\mid n}$ is the set of infinite sequence of colours that label paths from graphs of size at most $n$ satisfying $\Omega$.
Formally,
\[
\Omega^{\mid n} = \{\text{col}(\pi) \mid \pi \in \text{Path}_{\infty}(G), G \text{ has size at most $n$ and satisfies $\Omega$}\}.
\]

\begin{defi}
An $(n, \Omega)$-separating automaton $\mathcal{A}$ is a deterministic automaton such that
\[
\Omega^{\mid n} \subseteq L(\mathcal{A}) \subseteq \Omega.
\]
\end{defi}

The definition given here slightly differs from the original one given by Boja{\'n}czyk and Czerwi{\'n}ski~\cite{BC18},
who use a different relaxation $\Omega_n$ satisfying $\Omega^{\mid n} \subseteq \Omega_n \subseteq \Omega$.

\begin{thm}
\label{thm:separating_automata}
Let $\Omega$ be a positionally determined objective, $\mathcal{A}$ an $(n,\Omega)$-separating automaton, $\mathcal{G}$ a game of size $n$, and $v_0 \in V$. 
Then Eve wins from $v_0$ in $\mathcal{G}$ if and only if she wins from $(v_0,q_0)$ in $\mathcal{G} \triangleright \mathcal{A}$.
\end{thm}

We postpone the proof of Theorem~\ref{thm:separating_automata} to the next subsection which discusses the more general setting of GFSG automata.

\subsection{Good-for-small-games Automata}
\label{subsec:GFSG}
Good-for-small-games (GFSG) automata extend separating automata by introducing some (controlled) non-determinism.
The main motivation for doing so is that non-deterministic automata are more succinct than deterministic ones,
potentially leading to more efficient algorithms. 
The notion of good-for-small-games automata we introduce here is inspired by the notion of history-deterministic automata~\cite{HenzingerPiterman06}, and more precisely the variant called good-for-games automata used in the context of the theory of regular cost functions (\cite{Colcombet09}, see also~\cite{ColcombetF16}). 
We refer to Subsection~\ref{subsec:complexity_parity} for a discussion on the use of this model for solving parity games.

In a good-for-games automaton non-determinism can be resolved on the fly, only by considering the word read so far.
For GFSG automata, this property is only required for words in $\Omega^{\mid n}$.

\begin{defi}[Good-for-small-games automata]
An automaton $\mathcal{A}$ is $(n,\Omega)$-GFSG if it satisfies $\Omega$, and moreover, there exists a state $q_0$ and a partial map $\sigma_\mathcal{A} : C^+ \to Q$ such that for all $c_0 c_1 \dots \in \Omega^{\mid n}$, 
$q_0 c_0 q_1 \dots$ defines an infinite path in $\mathcal{A}$ with $q_i = \sigma_\mathcal{A}(c_0 \dots c_{i-1})$ for all $i \geq 1$.
\end{defi}

Note that $\sigma_\mathcal{A}$ is defined over all prefixes of $\Omega^{\mid n}$.
By a slight abuse, we refer to $\sigma_\mathcal{A}$ as the strategy of the $(n, \Omega)$-GFSG automaton $\mathcal{A}$.
This is justified by the fact that $\sigma_\mathcal{A}$ can formally be seen as a strategy in a game where 
Adam inputs colours and Eve builds a run in $\mathcal{A}$, and 
Eve wins if whenever the sequence of colours is in $\Omega^{\mid n}$ then the play is infinite.

If $\mathcal{A}$ is a separating automaton with initial state $q_0$, the partial map $w \mapsto \delta^*(q_0,w)$ is a strategy which indeed makes it GFSG. 
In this sense, the following theorem generalises Theorem~\ref{thm:separating_automata}.

\begin{thm}
\label{thm:GFSG_automata}
Let $\Omega$ be a positionally determined objective, $\mathcal{A}$ an $(n, \Omega)$-GFSG automaton, $\mathcal{G}$ a game of size $n$ and $v_0 \in V$. 
Then Eve has a winning strategy in $\mathcal{G}$ from $v_0$
if and only if she has a winning strategy in $\mathcal{G} \triangleright \mathcal{A}$ from $(v_0,q_0)$.
\end{thm}

\begin{proof}
The ``if'' follows directly from Lemma~\ref{lem:product_harder}. 
Conversely, we assume that Eve wins $\mathcal{G}$ from $v_0$, and let $\sigma$ be a winning strategy from $v_0$.
Since $\Omega$ is positionally determined, we can choose $\sigma$ to be positional.
We define a strategy $\sigma'$ over finite paths $\pi' = (v_0,q_0)(e_0,q_0) \dots$ with $e_i = (v_i,c_i,v_{i+1})$ for all $i$
and $\text{last}(\pi') \in \text{V}_{\text{Eve}}'$ as follows:
\[
\begin{array}{llll}
\sigma'(\pi') & = & (\sigma(v_i), q_i) & \text{ if } \text{last}(\pi') = (v_i,q_i) \in \text{V}_{\text{Eve}} \times Q, \\
\sigma'(\pi') & = & (v_{i+1}, \sigma_\mathcal{A}(c_0 \dots c_i))) & \text{ if } \text{last}(\pi') = (e_i,q_i) \in E \times Q.
\end{array}
\]
Intuitively, we simply play as prescribed by $\sigma$ on the first coordinate, and as prescribed by $\sigma_\mathcal{A}$ on the second.
We first show the following simulation property: 

\begin{center}
Let $\pi' = (v_0,q_0)(e_0,q_0) \dots (v_i,q_i)(e_i,q_i)$ \\
with $e_j = (v_j,c_j,v_{j+1})$ for all $j \le i$ be consistent with $\sigma'$, \\
then $\pi = v_0 c_0 \dots v_i c_{i+1} v_{i+1}$ is consistent with $\sigma$.
\end{center}

We proceed by induction over $i$, treating together the base case $i=0$ and the inductive case.
Let us consider $\pi'$ and $\pi$ as in the simulation property.
In both the base and inductive cases, $\pi_{\le i} = v_0 c_0 \dots c_{i-1} v_i$ is consistent with $\sigma$, either trivially or by inductive hypothesis.
There are two cases: either $v_i \in \text{V}_{\text{Adam}}$, and then since $\pi_{\le i}$ is consistent with $\sigma$ 
it follows that $\pi$ is consistent with $\sigma$,
or $v_i \in \text{V}_{\text{Eve}}$, and then since $\pi'$ is consistent with $\sigma'$ and by the first item of the definition of $\sigma'$ we have 
$\sigma(v_i) = e_i$, again $\pi$ is consistent with $\sigma$.
This concludes the inductive proof of the simulation property.

\vskip1em
We now show that $\sigma'$ is a winning strategy in $\mathcal{G} \triangleright \mathcal{A}$ from $(v_0,q_0)$.
Consider $\pi'$ a maximal consistent path in $\mathcal{G} \triangleright \mathcal{A}$ with $\sigma'$.
Since $\sigma'$ is defined over consistent paths ending in $\text{V}_{\text{Eve}}$, if, for contradiction, $\pi'$ is not winning in the safety game $\mathcal{G} \triangleright \mathcal{A}$, then it is finite and ends in a sink controlled by Eve.
There are two cases: either $\text{last}(\pi') = (v_i,q_i) \in \text{V}_{\text{Eve}} \times Q$, or $\text{last}(\pi') = (e_i,q_i) \in E \times Q$.

In the first case, the simulation property applied to 
$\pi' = (v_0,q_0)(e_0,q_0) \dots (e_{i-1},q_{i-1})$ 
implies that $\pi = v_0 c_0 \dots c_i v_i$ is consistent with $\sigma$.
Since $(v_i,q_i)$ is a sink this implies that $v_i$ is a sink (controlled by Eve), contradicting that $\sigma$ is a winning strategy from $v_0$.

In the second case the simulation property applied to
 $\pi' = (v_0,q_0)(e_0,q_0) \dots (v_i,q_i)(e_i,q_i)$
implies that $\pi = v_0 c_0 \dots v_i c_i v_{i+1}$ is consistent with $\sigma$.
In other words $\pi$ is a path in $\mathcal{G}[\sigma, v_0]$.
Since $\mathcal{G}[\sigma, v_0]$ is a graph satisfying $\Omega$ of size at most $n$, 
we have that $\text{col}(\pi) = c_0 \dots c_i$ is a prefix of a word in $\Omega^{\mid n} \subseteq L(\mathcal{A})$.
This implies that $\sigma_\mathcal{A}(c_0 \dots c_i)$ is well defined, hence so is $\sigma'(\pi')$,
thus $\text{last}(\pi')$ cannot be a sink.
\end{proof}



\subsection{Universal graphs}
\label{subsec:universal}

In comparison with separating and GFSG automata, the notion of universal graphs is more combinatorial than automata-theoretic, hence the name.
However, recall that in our formalism, non-deterministic automata and graphs are syntactically the same objects.

\paragraph*{Graph homomorphisms}
For two graphs $G,G'$, a homomorphism $\phi : G \to G'$ maps the vertices of $G$ to the vertices of $G'$ such that 
\[
(v,c,v') \in E \ \implies\ (\phi(v),c,\phi(v')) \in E'.
\]

As a simple example, note that if $G$ is a subgraph of $G'$, then the identity is a homomorphism $G \to G'$.
We say that $G$ maps into $G'$ if there exists a homomorphism $G \to G'$.

\begin{fact}
If $G$ maps into $G'$, then $L(G) \subseteq L(G')$.
\end{fact}

\begin{defi}[Universal graphs]
A graph $\mathcal{A}$ is $(n,\Omega)$-universal if it satisfies $\Omega$ and all graphs of size at most $n$ satisfying $\Omega$ map into $\mathcal{A}$.
\end{defi}

\begin{thm}
Let $\Omega$ be a positionally determined objective, $\mathcal{A}$ an $(n,\Omega)$-universal graph, $\mathcal{G}$ be a game of size $n$, and $v_0 \in V$.
Then Eve has a winning strategy in $\mathcal{G}$ from $v_0$ if and only if she has a winning strategy in $\mathcal{G} \triangleright \mathcal{A}$ from $(v_0,q_0)$ 
for some $q_0 \in Q$.
\end{thm}

\begin{proof}
Again, the ``if'' is a direct application of Lemma~\ref{lem:product_harder}.
Conversely, assume that Eve wins $\mathcal{G}$ from $v_0$, and let $\sigma$ be a winning strategy from $v_0$.
Since $\Omega$ is positionally determined, we can choose $\sigma$ to be positional.
Consider the graph $\mathcal{G}[\sigma,v_0]$: it has size at most $n$ and since $\sigma$ is winning from $v_0$ it satisfies $\Omega$.
Because $\mathcal{A}$ is an $(n,\Omega)$-universal graph there exists a homomorphism $\phi$ from $\mathcal{G}[\sigma,v_{\text{init}}]$ to~$\mathcal{A}$. 
We construct a positional strategy $\sigma'$ in $\mathcal{G} \triangleright \mathcal{A}$ 
by playing as in $\sigma$ in the first component and following the homomorphism $\phi$ on the second component. Formally,
\[
\begin{array}{llll}
\sigma'(v,q) &=& (\sigma(v),q) & \text{ for } v \in \text{V}_{\text{Eve}} \text{ and } q \in Q, \\
\sigma'(e,q) &=& (v', \phi(v')) & \text{ for } e=(v,c,v') \in E
 \text{ and } q \in Q.
\end{array}
\]
Let $q_0 = \phi(v_0)$. We first obtain the following simulation property by a straightforward induction: 
\begin{center}
Let $\pi' = (v_0,q_0)(e_0,q_0) \dots (v_i,q_i)(e_i,q_i)$ with $e_j = (v_j,c_j,v_{j+1})$ for all $j \le i$ be consistent with $\sigma'$, then \\
$\pi = v_0 c_0 \dots v_i c_{i+1} v_{i+1}$ is consistent with $\sigma$ and for all $j \le i$ we have 
$v_i \in V[\sigma, v_0], e_i \in E[\sigma, v_0]$, and $q_i = \phi(v_i)$.
\end{center}

We now show that $\sigma'$ is a winning strategy from $(v_0,q_0)$ in $\mathcal{G} \triangleright \mathcal{A}$.
Let $\pi'$ be a maximal consistent path with $\sigma'$, which we assume for contradiction to be losing, hence finite and ending in a sink controlled by Eve.
There are two cases: either $\text{last}(\pi') = (v_i,q_i) \in \text{V}_{\text{Eve}} \times Q$, or $\text{last}(\pi') = (e_i,q_i) \in E \times Q$.
In the first case, thanks to the simulation property this implies that $v_i$ is a sink, which contradicts that $\sigma$ is winning.
In the second case, let us note that since $\phi$ is a homomorphism and $e_i = (v_i,c_i,v_{i+1}) \in E[\sigma, v_0]$, 
we have $(\phi(v_i),c_i,\phi(v_{i+1})) \in \Delta$, 
so $\sigma'(e_i,q_i)$ is an edge from $(e_i,q_i)$ in $\mathcal{G} \triangleright \mathcal{A}$,
hence $(e_i,q_i)$ is not a sink, a contradiction.
\end{proof}


\subsection{Saturated graphs and linear graphs}
\label{subsec:saturated_graphs_and_linear_graphs}

We introduce the two most important concepts of this Section~\ref{sec:saturation}: saturated graphs and linear graphs.
Given a graph $G$ and $e \notin E$, we let $G_e$ denote the graph $(V,E \cup \set{e})$.

\begin{defi}[Saturated graphs]
A graph $G$ is saturated with respect to $\Omega$ if $G$ satisfies $\Omega$ and for all $e \notin E$ we have that 
$G_e$ does not satisfy $\Omega$.
\end{defi}

Let $G$ a graph satisfying $\Omega$, we say that $\widehat{G}$ is a saturation of $G$ if 
$\widehat{G}$ is saturated, uses the same set of vertices as $G$, and all edges of $G$ are in $\widehat{G}$.

\begin{lem}
\label{lem:saturation}
Let $G$ be a graph satisfying $\Omega$. 
Then there exists a saturation $\widehat{G}$ of $G$, and the identity is a homomorphism from $G$ to $\widehat{G}$.
\end{lem}

\begin{proof}
There are finitely many graphs over the set of vertices of $G$ which include all edges of $G$, so there exists a maximal one with respect to edge inclusion for the property of satisfying $\Omega$. 
\end{proof}

The following two facts will be very useful for reasoning, they essentially say that in the context of universal graphs, 
we can restrict our attention to saturated graphs without of loss of generality.

\begin{fact}
Let $n \in \mathbb N$, $\Omega$ an objective, and $\mathcal U$ a graph.
\begin{itemize}
	\item If $\mathcal U$ is an $(n,\Omega)$-universal graph, then any saturation of $\mathcal U$ is $(n,\Omega)$-universal and has the same size as $\mathcal U$,
	\item the graph $\mathcal U$ is $(n,\Omega)$-universal if and only if 
	it satisfies $\Omega$ and all saturated graphs $G$ of size $n$ map into $\mathcal U$. 
\end{itemize}
\end{fact}
Both are consequences of the following observation: if a saturation $\widehat{G}$ of $G$ maps into $\mathcal U$,
then $G$ maps into $\mathcal U$ by composing the homomorphisms from $G$ to $\widehat{G}$ and from $\widehat{G}$ to $G$.

We will see that saturated graphs satisfy structural properties captured by the following definition.

\begin{defi}[Linear graphs]
A graph $G$ is linear if there exists a total order $\le$ on the vertices of $G$ satisfying the following two properties:
\begin{eqnarray*}
\text{ if } v \ge v' \text{ and } (v',c, v'') \in E, \text{ then } (v, c, v'') \in E, \\
\text{ if } (v ,c , v') \in E \text{ and } v' \ge v'', \text{ then } (v, c, v'') \in E.
\end{eqnarray*}
We refer to the first property as left composition and to the second as right composition.
\end{defi}

Given a linear graph $G$, a vertex $v \in V(G)$ and a colour $c \in C$, one may define the set of $c$-successors of $v$, $\{v' \in V(G) \mid (v,c,v') \in E(G)\}$, which by right composition is downward closed with respect to the order on $G$. 
Hence it is uniquely defined by its maximal element, which we refer to as $\delta(v,c) \in V(G) \cup \{\bot\}$.
Likewise, the set of $c$-predecessors of $v' \in V(G)$, given by $\{v \in V(G) \mid (v,c,v') \in E(G)\}$ is upwards closed by left composition. We let $\rho(v',c) \in V(G) \cup \{\top\}$ denote the minimal $c$-predecessor of $v'$.

For a fixed $c \in C$, the functions $v \mapsto \delta(v,c)$ and $v' \mapsto \rho(v',c)$ are non-decreasing, respectively thanks to left and right composition. If it holds for some $v,v'$ that for all colours $c$, we have $\delta(v,c)=\delta(v',c)$, and $\rho(v,c) = \rho(v',c)$, then $v, v'$, and any vertex $v''$ between $v$ and $v'$ all have exactly the same incoming and outgoing edges.



The operator $\delta(\cdot,c)$ also allows us to determinise linear graphs while preserving the state space.

\begin{defi}[Determinisation of linear graphs]
Let $G$ be a linear graph with respect to $\leq$. 
We define its determinisation $\text{Det}(G)$ by $\text{Det}(G) = (V(G), \delta, v_0)$ with $v_0$ the maximum element of $V$ 
and where $\delta(v,c)$ is defined as the largest $c$-successor of $v$ if there is any (and undefined otherwise).
\end{defi}

\begin{lem}\label{lem:determinisation}
Let $G$ be a linear graph. Then $G$ and $\text{Det}(G)$ recognise the same language.
\end{lem}

\begin{proof}
It is clear that $L(\text{Det}(G)) \subseteq L(G)$. Conversely, let $\pi = v_0 c_0 v_1 c_1 \dots$ be a path in $G$. 
We prove by induction that for all $i$, $\delta^*(v_0,c_0 \dots c_i)$ is well defined and greater than or equal to $v_i$. 
This is clear for $i = 0$, so let us consider $i > 0$. 
Since $(v_i,c_i,v_{i+1}) \in E$ and by induction hypothesis $\delta^*(v_0,c_0 \dots c_i) \ge v_i$,
we have by left composition that $(\delta^*(v_0,c_0 \dots c_i), c_i, v_{i+1}) \in E$. 
Hence $\delta^*(v_0,c_0 \dots c_{i+1})$ is well defined and greater than or equal to $v_{i+1}$, which concludes the inductive proof. 
This implies that $c_0 c_1 \dots \in L(\text{Det}(G))$.
\end{proof}

\subsection{Normalisation theorem}
\label{subsec:saturated_graphs_are_linear_graphs}

We now prove our normalisation result.

\begin{thm}
\label{thm:saturated_graphs_are_linear}
Let $\Omega$ be a prefix independent and positionally determined objective with a neutral letter. Then any saturated graph with respect to $\Omega$ is linear.
\end{thm}

This theorem is the only place in the paper where we use the neutral letter.


\begin{proof}
Let $G$ be a saturated graph, and consider the relation $\leq$ over $V(G)$ given by $v \geq v' \iff (v,0,v') \in E(G)$. We now prove that $\leq$ is a total preorder satisfying left and right composition.
\begin{itemize}
	\item \textbf{Reflexivity}. Let $v \in V$. We argue that $(v,0,v) \in E$. 
	Indeed if this were not the case then adding it to $G$ would create a graph satisfying $\Omega$ by definition of $\Omega$, which contradicts the fact that $G$ is saturated.
	
	\item \textbf{Totality}. Assume for contradiction that neither $(v,0,v') \in E$ nor $(v',0,v) \in E$.

	We construct a game $\mathcal{G}$ with objective $\Omega$. See Figure~\ref{fig:question_mark_game}.
	
	\begin{figure}
	\includegraphics[width= 0.7 \linewidth]{Fig/question_mark_game.eps}
	\caption{On the left the graph $G$, and on the right the game $\mathcal{G}$. The circle depicts the unique vertex which belongs to Eve, while squares belong to Adam.}
	\label{fig:question_mark_game}
	\end{figure}	
	
	
	The underlying graph is obtained from $G$ with the following modification: 
	the set of vertices is $V$ plus a new vertex $v_?$.
	All vertices are controlled by Adam except for the new vertex $v_?$.
	For every edge leading to either $v$ or $v'$, we add a new edge going to $v_?$,
	where Eve chooses between going to $v$ or to $v'$ with colour $0$.
	Formally, the sets of vertices and edges are
	\[
	\begin{array}{lll}
	\text{V}_{\text{Eve}} & = & \{v_?\} \\
	\text{V}_{\text{Adam}} & = & V \\
	E' & = & E \cup \{(u,c,v_?) : (u,c,v) \in E \text{ or } (u,c,v') \in E\} \cup  \{(v_?,0,v), (v_?,0,v')\}.
	\end{array}
	\]
	Eve has a winning strategy from any vertex $v \in V$: each time the path reaches $v_?$ from an edge $(u,c,v_?)$ such that 
	$(u,c,v) \in E$, Eve chooses to continue with $v$, and otherwise with $v'$. 
	Any path consistent with this strategy corresponds to a path in $G$,
	and since $G$ satisfies $\Omega$ this strategy is winning.
	We note that this strategy is not positional as it chooses $v$ or $v'$ depending on the incoming edge.
	
	We claim that Eve does not have a positional winning strategy in $\mathcal{G}$, 
	which contradicts the positional determinacy of $\Omega$.
	Indeed, if the positional strategy defined by $\sigma(v_?) = v$ were winning, 
	since any path in $G_{(v',0,v)}$ is consistent with $\sigma$ in $\mathcal{G}$, 
	this would imply that $G_{(v',0,v)}$ satisfies $\Omega$, contradicting the maximality of $G$.
	The same argument leads to a contradiction if $\sigma(v_?) = v'$ is a winning strategy.
	
	\item \textbf{Generalised transitivity}. 
	Note that left and right composition both generalise transitivity of $\leq$, that is, $(v,0,v') \in E(G)$ (1) and $(v',0,v'') \in E(G)$ (2) implies $(v,0,v'') \in E(G)$ (3), by replacing, respectively in (2) or in (1), and in the conclusion (3), the colour 0 with any colour $c$.
	We prove left composition.
	Assume that $(v,0,v') \in E$ and $(v',c,v'') \in E$.
	We argue by contradiction that $(v,c,v'') \in E$. 
	Assuming otherwise, consider a path $\pi$ in $G_{(v,c,v'')}$. 
	Then $\pi'$ obtained from $\pi$ by replacing all occurrences of $v c v''$ by $v 0 v' c v''$ is a path in $G$ 
	so it must satisfy $\Omega$ and hence $\pi$ as well. 
	This contradicts the maximality of $G$.
	The proof of right composition follows the same lines.
\end{itemize}

Now to obtain a total order it suffices to refine $\leq$ arbitrarily over its equivalence classes, which preserves left and right compositions. Indeed, two vertices are equivalent for $\leq$ (before refining), that is, are interconnected with $0$-edges, if and only if they have exactly the same $c$-successors and $c$-predecessors for all colours $c$.
\end{proof}




\subsection{Ubiquity of linear graphs}
\label{subsec:linear_graphs_are_everywhere}

We now relate linear graphs to the models of Section~\ref{sec:reductions}.

\begin{lem}
\label{lem:linear_graphs_are_everywhere}
Let $\mathcal{A}$ be a linear graph such that $\Omega^{\mid n} \subseteq L(\mathcal{A}) \subseteq \Omega$. Then
\begin{itemize}
	\item $\text{Det}(\mathcal{A})$ is an $(n,\Omega)$-separating automaton,
	\item $\mathcal{A}$ is an $(n, \Omega)$-GFSG automaton, and
	\item $\mathcal{A}$ is an $(n, \Omega)$-universal graph.
\end{itemize}
\end{lem}

\begin{proof}
By Lemma~\ref{lem:determinisation}, $L(\text{Det}(\mathcal{A})) = L(\mathcal{A})$, so the first item is clear.
The second item follows by using the strategy induced by the determinised automaton, that is, 
$\sigma_{G}(c_0 \dots c_i) = \delta^*(v_0, c_0 \dots c_i)$.

We now focus on the third item.
Let $G$ be a graph satisfying $\Omega$ and of size at most $n$, and let $v \in V$.

Let $\pi = v_0 c_0 \dots c_{i} v$ be a path ending in $v$ in $G$. 
Then $\text{col}(\pi) = c_0 \dots c_{i}$ is a prefix of a word in $\Omega^{\mid n}$, so $\delta^*(v_0, \text{col}(\pi))$ is well defined.
We now let $\phi : V \to Q$ be defined by
\[
\phi(v) = \min \set{\delta^*(v_0, \text{col}(\pi)) : \pi \text{ is a path in $G$ ending in $v$}}.
\]
Note that there is always a path ending in $v$ since $v$ itself is such a path.

We now prove that $\phi$ defines a graph homomorphism.
Let $(v,c,v') \in E$, and let $\pi_v$ be a path in $G$ ending in $v$ such that 
$\phi(v) = \delta^*(v_0, \text{col}(\pi_v))$. 
Then $\pi_v c v'$ is a path in $G$ ending in $v'$ with colour $\text{col}(\pi_v) c$, so we have 
$\phi(v') \leq \delta^*(v_0, \text{col}(\pi_v) c) = \delta(\phi(v), c)$, and by left composition 
$(\phi(v), c, \phi(v')) \in Q$.
This shows that $\phi$ is a homomorphism from $G$ to $\mathcal{A}$, so $\mathcal{A}$ is indeed $(n,\Omega)$-universal.
\end{proof}

We now obtain Theorem~\ref{thm:main} as a direct consequence.

\begin{proof}
Let $\mathcal{A}$ be a non-deterministic automaton such that $\Omega^{\mid n} \subseteq L(\mathcal{A}) \subseteq \Omega$. Note that this includes separating automata, GFSG automata and universal graphs. Saturate $\mathcal{A}$ (Lemma~\ref{lem:saturation}) to obtain (Theorem~\ref{thm:saturated_graphs_are_linear}) a linear graph. Lemma~\ref{lem:linear_graphs_are_everywhere} concludes.
\end{proof}


\subsection{Simplifying the product game if $\mathcal{A}$ is linear}
\label{subsec:simplification_linear}

We defined the product game $\mathcal{G} \triangleright \mathcal{A}$ for the general case of a non-deterministic automaton $\mathcal{A}$.
If $\mathcal{A}$ is linear, the product game can be simplified: from $(e,q)$ where $e=(v,c,v')$, Eve should always pick as large a successor in $Q$ as possible (if there is any successor).
More precisely, we let $\delta(q,c) = \max\{q' \in Q \mid (q,c,q') \in \Delta\}$ 
and consider the safety game $\mathcal{G} \ \tilde \chain \  \mathcal{A}$ with vertices $V' = \text{V}_{\text{Eve}}' \uplus \text{V}_{\text{Adam}}'$ and edges $E'$ given by
\[
\begin{array}{lll}
\text{V}_{\text{Eve}}' & = & \text{V}_{\text{Eve}} \times Q\ \cup \set{\bot}, \\
\text{V}_{\text{Adam}}' & = & \text{V}_{\text{Adam}} \times Q, \\
E' & = & \{((v,q), (v',\delta(q,c))) : q \in Q, (v,c,v') \in E, \delta(q,c) \text{ is defined}\} \\
 & \cup & \{((v,q), \bot) : q \in Q, (v,c,v') \in E, \delta(q,c) \text{ is not defined}\}.
\end{array}
\]

In words, from $(v,q) \in V \times Q$, the player whom $v$ belongs to chooses an edge $e=(v,c,v') \in E$, and the game progresses to $(v',\delta(q,c))$ if $q$ has an outgoing edge with colour $c$ in $\mathcal{A}$, and to $\bot$ otherwise, which is losing for Eve.

It is clear that Eve wins from $(v,q)$ in $\mathcal{G} \triangleright \mathcal{A}$ (as defined in Subsection~\ref{subsec:product}) 
if she wins from $(v,q)$ in $\mathcal{G} \ \tilde \chain \  \mathcal{A}$, simply by always choosing $\delta(q,c)$ as a successor from $(e,q)$ where $e = (v,c,v')$.
The converse is not much harder: just as in the proof of Lemma~\ref{lem:determinisation}, by an easy induction, picking the largest successor ensures to always remain larger on the second component, which allows for more possibilities (and in particular, avoids sinks) thanks to left composition.

\begin{remark}\label{rmk:upward-closed}
This also proves that if $(v,q)$ is in the winning region of $\mathcal{G} \triangleright \mathcal{A}$ and $q' \geq q$, then $(v,q')$ is also winning. In particular, $v$ is winning in $\mathcal{G}$ if and only if there exists $q \in Q$ such that $(v,q)$ is winning in $\mathcal{G} \triangleright \mathcal{A}$ if and only if $(v, \max Q)$ is winning in $\mathcal{G} \triangleright \mathcal{A}$.
\end{remark}

From here on, since we solve $\mathcal{G} \triangleright \mathcal{A}$ for linear $\mathcal{A}$, we shall use the new (simpler) definition $\ \tilde \chain \ $ instead of $\triangleright$.

\subsection{Solving safety games in linear time}
\label{subsec:safety_games}

We recall the standard linear time algorithm for safety games. Let $\mathcal{G}$ be a safety game, and consider the operator $\mathtt{Safe}$ over subsets of $V$ given by
\[
\begin{array}{lll}
\mathtt{Safe}(X) & = & \{v \in \text{V}_{\text{Eve}} \mid \exists v', (v,v') \in E\text{ and } v' \in X\} \\
& \cup & \{v \in \text{V}_{\text{Adam}} \mid \forall v', (v,v') \in E \implies v' \in X\},
\end{array}
\]
that is, $\mathtt{Safe}(X)$ is the set of vertices from which Eve can ensure to remain in $X$ for one step. 
Note that $\mathtt{Safe}(X)$ always includes sinks controlled by Adam and excludes sinks controlled by Eve,
and it is monotone: if $X \subseteq Y$, then $\mathtt{Safe}(X) \subseteq \mathtt{Safe}(Y)$.

It is well known that the winning region in $\mathcal{G}$ is the greatest fixpoint of $\mathtt{Safe}$. This can be computed via Kleene iteration by setting $X_0=V$ and $X_{i+1} = \mathtt{Safe}(X_i)$, which stabilizes in at most $|V|$ steps. Since computing $\mathtt{Safe}$ requires $O(|E|)$ operations, a naive implementation yields runtime $O(|V| \cdot |E|)$.

To obtain linear runtime $O(|E|)$, let us define $R_i = X_{i} \setminus X_{i+1}$, the set of vertices which are removed upon applying $\mathtt{Safe}$ for the $(i+1)$\textsuperscript{-th} time (see Figure~\ref{fig:safety_game}).
Then $R_0$ is the set of sinks controlled by Eve, and moreover we show that for $i \geq 1$, $R_i$ can be computed efficiently from $R_{i-1}$, provided one maintains a data structure $\texttt{Count}$, which stores, for each $v \in \text{V}_{\text{Eve}}$, the number of edges from $v$ to $X_i$. This is based on the observation that a vertex in $\text{V}_{\text{Adam}} \cap X_i$ belongs to $R_i$ if and only if it has an edge towards $R_{i-1}$, and a vertex in $\text{V}_{\text{Eve}} \cap X_i$ belongs to $R_i$ if and only if it has no outgoing edge towards $X_i$, and moreover it has an edge towards $R_{i-1}$ (otherwise, it would not belong to $X_i$).

Hence to compute $R_i$ and update $\texttt{Count}$, it suffices to iterate over all edges $e=(v,v')$ such that $v' \in R_{i-1}$ and $v \in X_i$: if $v \in \text{V}_{\text{Adam}}$ then $v \in R_i$, and if $v \in \text{V}_{\text{Eve}}$, then $\texttt{Count}(v)$ is decremented, and $v$ is added to $R_i$ if 0 is reached, that is, $v$ has no edge going to $X_i$. We give a pseudo-code in Appendix~\ref{sec:safety} for completeness.
The overall linear complexity of the algorithm simply follows from the fact that each edge is considered at most once.

\begin{figure}
\includegraphics[width = 0.8 \linewidth]{Fig/safety_game.eps}
\caption{Example of a safety game, where Eve vertices are depicted with circles and Adam vertices with squares. The iteration terminates after 4 steps: $X_4 = \mathtt{Safe}(X_4)$. In this example, $\texttt{Count}(u)$ is initialized at two, decremented when $w$ is added to $R_0$, and decremented again, reaching 0, when $v$ is added to $R_1$. Hence $u$ is then added to $R_2$. In contrast, $\texttt{Count}(u')$ never reaches 0 thanks to the edge towards $v'$.}
\label{fig:safety_game}
\end{figure}


\subsection{Instantiating to $\mathcal{G} \triangleright \mathcal{A}$: a space efficient implementation}
\label{subsec:space-efficiency}

We now instantiate the previous algorithm for safety games to $\mathcal{G} \triangleright \mathcal{A}$ 
as defined in~\ref{subsec:simplification_linear}.

For a vertex $v \in V$ and a set $X$ of vertices of $\mathcal{G} \triangleright \mathcal{A},$ we let $X^v = \set{q \in Q \mid (v,q) \in X}$. 
As we have discussed (see Remark~\ref{rmk:upward-closed}), the winning region $W$ is such that $W^v$ is upward-closed for all $v$.
We will see that when instantiating the previous algorithm to $\mathcal{G} \triangleright \mathcal{A}$, that is, letting $X_0 = V(\mathcal{G} \triangleright \mathcal{A})$ and $X_{i+1} = \mathtt{Safe}(X_i)$, it always holds that $X_i^v$ is upward-closed for all $v$, and hence it is specified by its minimal element.
Given $X$ such that $X^v$ is upward-closed for all $v$, we let $\theta_X : V \to Q \cup \{\top\}$ be defined by $\theta(v)=\min X^v$, with value $\top$ if $X^v = \emptyset$.
We now characterize the effect of $\mathtt{Safe}$ over sets represented in this manner.
Recall that $\rho(q',c)=\min\{q \in Q \mid (q,c,q') \in \Delta\} \in \mathbb Q \cup \{\top\}$.

\begin{lem}\label{lem:charac_update}
Let $X$ be such that $X^v$ is upward-closed for all $v$, and let $X'=\mathtt{Safe}(X)$. Then $X'^v$ is upward-closed for all $v$, and $\theta_{X'}$ is given by
\[
\theta_{X'}(v)=
\begin{cases}
\min\{\rho(\theta_X(v'),c), (v,c,v') \in E\} $ if $ v \in \text{V}_{\text{Eve}}, \\
\max\{\rho(\theta_X(v'),c), (v,c,v') \in E\} $ if $ v \in \text{V}_{\text{Adam}}.
\end{cases}
\]
\end{lem}

\begin{proof}
Note that for $q,q' \in Q$ and $c \in C$ we have
\[
\delta(q,c) \geq q' \iff (q,c,q') \in \Delta \iff q \geq \rho(q',c),
\]
where the first equivalence holds by right composition while the second holds by left composition.

Let $v \in \text{V}_{\text{Eve}}$. Then
\[
\begin{array}{lll}
(v,q) \in X' =  \mathtt{Safe}(X) & \iff & (v,q) \text{ has an edge to } X \text{ in } \mathcal{G} \triangleright \mathcal{A} \\
& \iff & \exists (v,c,v') \in E, (v', \delta(q,c)) \in X \\
& \iff & \exists (v,c,v') \in E, \delta(q,c) \geq \theta(v') \\
& \iff & \exists (v,c,v') \in E, q \geq \rho(\theta(v'),c)
\end{array}
\] 
Hence, $X'^v$ is upward-closed, and given by
\[
\theta_{X'}(v) = \min \set{q \in Q \mid (v,q) \in \mathtt{Safe}(X)} = \min \set{\rho(\theta(v'),c) : (v,c,v') \in E}.
\]
For $v \in \text{V}_{\text{Adam}}$ replacing $\exists$'s by $\forall$'s in the previous chain of equivalences yields 
\[
\theta_{X'}(v) = \min \set{q \in Q \mid (v,q) \in \mathtt{Safe}(X)} = \max \set{\rho(\theta(v'),c) : (v,c,v') \in E}.
\]
\end{proof}

Let $X_0=V(\mathcal{G} \triangleright \mathcal{A})$ and $X_{i+1}=\mathtt{Safe}(X)$.
By a straightforward induction, for all $i$ and all $v$, $X_i^v$ is upward-closed, and we let $\theta_i = \theta_{X_i}$.
By the above lemma, for each $v$, $\theta_{i+1}(v)$ can be computed from the value of $\theta_i$ at each successor $v'$ of $v$.
Note that by monotonicity of $\mathtt{Safe}$, for each $v$ we have $\theta_{i+1}(v) \geq \theta_i(v)$.
Following the usual terminology for value iteration algorithms, we say that a vertex $v$ is invalid at step $i$ if $\theta_{i+1}(v) > \theta_{i}(v)$, or equivalently, $(v,\theta_i(v)) \in X_i \setminus \mathtt{Safe}(X_i)$.
We let $\mathrm{Inv}_i \subseteq V$ denote the set of vertices which are invalid at step $i$.
To compute $\theta_{i+1}$ from $\theta_i$, it suffices to update the value of $\theta_i(v)$ for each $v \in \mathrm{Inv}_i$. See Figure~\ref{fig:product_safety_game}.

\begin{figure}
\includegraphics[width = 0.8 \linewidth]{Fig/product_safety_game.eps}
\caption{Computing the $i$-th layer in the safety game $\mathcal{G} \triangleright \mathcal{A}$. For each $v$, $X_i^v$ is upward-closed, and $X$ is represented by $\theta:V \to Q \cup \{\top\}$. The blue squares represent vertices of the form $(v,\theta(v))$, which lie at the border of $X_i$. The hatched area represents the $i$-th layer $X_i \setminus X_{i+1}$. Computing the position of the red squares, given by $\theta'$, is achieved using lemma~\ref{lem:charac_update}. Computing the new set $\mathrm{Inv}_{i+1}$ of invalid vertices is achieved by inspecting $c$-predecessors $u$ in $\mathcal{G}$ of each $u' \in \mathrm{Inv}_i$: if $\theta(u') \leq \delta(u,c) < \theta'(u')$, then there was an edge in $\mathcal{G} \triangleright \mathcal{A}$ from $(u,\theta(u))$ towards $X_i^{u'}$, but there is no edge from $(u,\theta'(u))$ to $X_{i+1}^{u'}$. Hence, if $u \in \text{V}_{\text{Adam}}$ it is added to $\mathrm{Inv}_{i+1}$, and if $u \in \text{V}_{\text{Eve}}$, $\texttt{Count}(u)$ is decremented, and $u$ is added to $\mathrm{Inv}_{i+1}$ if 0 is reached.}
\label{fig:product_safety_game}
\end{figure}

Following the previous generic linear time algorithm for solving safety games, we store for each Eve vertex the number of edges from $(v,\theta_i(v))$ to $X_i$, which allows to efficiently compute the set of vertices which are invalid at step $i$ from those which are invalid at step $i-1$. We again give a full pseudo-code in Appendix~\ref{sec:product_safety}.

Let us conclude with analysing the complexity of the generic value iteration algorithm
in the RAM model with word size $w = \log(|V|) + \log(|Q|)$, in which computing $\delta$ and $\rho$, checking whether $q \le q'$ and evaluating $\theta$ require constant time, while storing $\theta$ requires space linear in $|V|$.

Note that at step $i$, each vertex $v \in \mathrm{Inv}_i$ sees a strict increase in $\theta_i(v) \in Q \cup \{\top\}$. Hence, there is at most $|Q|+1$ values of $i$ such that $v \in \mathrm{Inv}_i$. Moreover, computing the $i$\textsuperscript{th} update requires, for each $v \in \mathrm{Inv}_i$, $O(\text{out-deg}(v))$ constant-time operations for computing $\theta'(v)$, and $O(\text{in-deg}(v) + \text{out-deg}(v))$ constant-time operations for updating $\texttt{Count}$ (at $v$ and its predecessors) and computing $\mathrm{Inv}_{i+1}$.

Summing over all vertices, we obtain the wanted $O(|E| \cdot |Q|)$ time complexity.

\begin{remark}
The value iteration algorithm we present here instantiates a linear time implementation of the (global) fixpoint computation $X_{i+1} = \mathtt{Safe}(X)$ to the safety game $\mathcal{G} \triangleright \mathcal{A}$. There exists a variation of this algorithm which also achieves linear time for solving generic safety games, and works locally: keep a queue $R$ of vertices which should be removed from $X$, and a data structure $\texttt{Count}$ storing the number of outgoing edges from $v \in \text{V}_{\text{Eve}}$ to $X$ and iteratively pick a vertex from $R$, remove it from $X$, and update $\texttt{Count}$ (potentially adding them to $R$) on each predecessor of $v$.

It is not hard to instead adapt the local variant of the algorithm to the safety game $\mathcal{G} \triangleright \mathcal{A}$, which yields another slightly different generic value iteration procedure (with same complexity). The local variant is more in line with known value iteration algorithms for parity games~\cite{J00,JL17,FJSSW17} as well as mean-payoff games~\cite{BCDGR11,DKZ19}. We chose to present the global variant for its structural simplicity, and direct ties with the fixpoint iteration. For details about the local variant of the generic algorithm, we refer to~\cite{FGO18}.\end{remark}

This concludes the first part of the paper developing the theory of universal graphs.
In the second part, we will consider four (classes of) objectives and construct algorithms from universal graphs.