\section{Proof of Proposition \ref{prop:merging}}\label{app:merging}

\begin{refproposition}{prop:merging}
	The color summary of the run DAG $G_w^*$ is even if and only if there is an accepting run in $G_w$.
\end{refproposition}
\begin{proof}
	``$\Rightarrow$'':
	The `only-if' direction can be proven as in Theorem~\ref{thm:coloring} verbatim, only replacing $G_w$ by $G_w^*$.
	The reason why the argumentation is still correct, is that the discussed ``smallest run prefix that ends up in $v$'' (now in $G_w^*$) is actually a real run prefix (in $G_w$) since it never secondarily merged. Indeed, runs only merge into smaller ones.
	
	``$\Leftarrow$'':
	(Step 1):
	For the `if' direction, we first use the proof Theorem~\ref{thm:coloring}, Step 1, verbatim, obtaining the smallest accepting run in $G_w$.
	
	Additionally, we prove that this (smallest) constructed run $\rho$ is actually a run in $G_w^*$. 
	For a contradiction, assume that this is not the case and $\rho=\rho_1 (v_k,i) \rho_2$ where $(v_k,i)$ is the first vertex on $\rho$ that secondarily merged.
	Then there is $(v_j,i)\in V_i\cap(Q_d\times\{i\})$ with $v_j\sqsubset v_k$ and $\mathsf{L}(v_j)$ contains the label of the run $(v_k,i) \rho_2$, accepted by some run $(v_j,i)\rho_2'$ in $G_w$.
	Since $(v_j,i)\sqsubset_i(v_k,i)$, we also have a run prefix $\rho_1'(v_j,i)\sqsubset\rho_1(v_k,i)$, and thus an accepting run $\rho_1'(v_j,i)\rho_2'$ in $G_w$ such that $\rho_1'(v_j,i)\rho_2'\sqsubset \rho_1 (v_k,i) \rho_2=\rho$, a contradiction with minimality of $\rho$. 
	
	(Step 2): Let $k$ be the position when the last merge of a smaller run pefix happens in $G_w^*$ (not $G_w$).
	
	(Step 3): We use the proof Theorem~\ref{thm:coloring}, Step 3, verbatim, proving the color summary is even.	
	\qed
\end{proof}

\section{Proof of Proposition \ref{prop:translation}}\label{app:ltl}

We start by recalling the LTL$\rightarrow$LDBA translation of \cite{DBLP:conf/cav/SickertEJK16}.

\paragraph{Preliminaries.} 
The translation assumes that formulas are in {\em negation normal form}, given 
by the syntax
\begin{align*}
\varphi::= & \; {\ensuremath{\mathbf{tt}}} \mid {\ensuremath{\mathbf{ff}}} \mid a \mid \neg a \mid \varphi\wedge\varphi \mid \varphi\vee\varphi \mid {\ensuremath{\mathbf{X}}}\varphi \mid {\ensuremath{\mathbf{F}}}\varphi \mid {\ensuremath{\mathbf{G}}}\varphi \mid \varphi{\ensuremath{\mathbf{U}}}\varphi
\end{align*}
\noindent where $a$ belongs to a finite set of atomic propositions. Every formula over the usual 
syntax of LTL (with negation and the ${\ensuremath{\mathbf{X}}}$ and ${\ensuremath{\mathbf{U}}}$ operators) can be normalized with linear blowup 
if formulas are represented by their syntax DAGs, where two occurrences of the same subformula are
represented by the same node.

We recall the ${\it af}$ function introduced in \cite{DBLP:conf/cav/EsparzaK14,DBLP:conf/cav/SickertEJK16},
and some of its properties. Let $\nu$ be a letter. The formula 
${\it af}(\varphi,\nu)$, read ``$\varphi$ after $\nu$'' is  inductively defined as follows \cite{DBLP:conf/cav/EsparzaK14,DBLP:conf/cav/SickertEJK16}:
\[\begin{array}[t]{lcl}
{\it af}({\ensuremath{\mathbf{tt}}},\nu)& = & {\ensuremath{\mathbf{tt}}} \\[0.1cm]
{\it af}({\ensuremath{\mathbf{ff}}},\nu)& = & {\ensuremath{\mathbf{ff}}} \\[0.1cm]
{\it af}(a,\nu)& = & \left\{
\begin{array}{ll}
{\ensuremath{\mathbf{tt}}} & \mbox{if $a \in \nu$} \\[0.1cm]
{\ensuremath{\mathbf{ff}}} & \mbox{if $a \notin \nu$}\end{array}\right. \\[0.3cm]
{\it af}(\neg a,\nu)&=& \left\{
\begin{array}{ll}
{\ensuremath{\mathbf{ff}}} & \mbox{if $a \in \nu$} \\ [0.1cm]
{\ensuremath{\mathbf{tt}}} & \mbox{if $a \notin \nu$}\end{array}\right. \\[0.3cm]
\end{array} 
\hspace{0.5cm}
\begin{array}[t]{lcl}
{\it af}(\varphi\wedge\psi,\nu)&=& {\it af}(\varphi,\nu)\wedge{\it af}(\psi,\nu) \\[0.1cm]
{\it af}(\varphi\vee\psi,\nu)&=& {\it af}(\varphi,\nu)\vee{\it af}(\psi,\nu) \\[0.1cm]
{\it af}({\ensuremath{\mathbf{X}}}\varphi,\nu)& = &  \varphi\\[0.1cm]
{\it af}({\ensuremath{\mathbf{G}}}\varphi,\nu)&= & {\it af}(\varphi,\nu)\wedge {\ensuremath{\mathbf{G}}}\varphi\\[0.1cm]
{\it af}({\ensuremath{\mathbf{F}}}\varphi,\nu)&= & {\it af}(\varphi,\nu)\vee {\ensuremath{\mathbf{F}}}\varphi\\[0.1cm]
{\it af}(\varphi{\ensuremath{\mathbf{U}}}\psi,\nu)&=& {\it af}(\psi,\nu)\vee({\it af}(\varphi,\nu)\wedge \varphi{\ensuremath{\mathbf{U}}}\psi)
\end{array}\]
Furthermore, we define: ${\it af}(\varphi, \epsilon) = \varphi$, and
${\it af}(\varphi, \nu w) = {\it af}({\it af}(\varphi,\nu), w)$ for every letter $\nu$ and every finite word $w$.
The function ${\it af}$ has the following two properties \cite{DBLP:conf/cav/EsparzaK14,DBLP:conf/cav/SickertEJK16}
for every formula $\varphi$, finite word $v$, and $\omega$-word $w$:
\begin{itemize}
	\item[(i)]  $vw \models \varphi$ if{}f $w \models {\it af}(\varphi,v)$.
	\item[(ii)]  ${\it af}(\varphi, v)$ is a boolean combination of subformulas of $\varphi$.
\end{itemize}

A formula is {\em proper} if it is neither a conjunction nor a disjunction.
The propositional formula $\varphi_P$ of a formula $\varphi$ is the result of
substituting every maximal proper subformula $\psi$ of $\varphi$ by a propositional variable $x_\psi$. 
For example, if $\varphi = {\ensuremath{\mathbf{X}}} b \vee ({\ensuremath{\mathbf{G}}}(a \vee {\ensuremath{\mathbf{X}}} b) \wedge {\ensuremath{\mathbf{X}}} b)$ with $\psi_1 = {\ensuremath{\mathbf{X}}} b$ and $\psi_2 = {\ensuremath{\mathbf{G}}}(a \vee {\ensuremath{\mathbf{X}}} b)$, 
then $\varphi_P = x_{\psi_1} \vee (x_{\psi_2} \wedge x_{\psi_1})$. 
Two formulas $\varphi, \varphi'$ are {\em propositionally equivalent}, denoted $\varphi \equiv_P \varphi'$, 
if $\varphi_P$ and $\varphi'_P$ are equivalent. 
So, for example, ${\ensuremath{\mathbf{X}}} b$ is propositionally equivalent to ${\ensuremath{\mathbf{X}}} b \vee ({\ensuremath{\mathbf{G}}}(a \vee {\ensuremath{\mathbf{X}}} b) \wedge {\ensuremath{\mathbf{X}}} b)$.
Observe that propositional equivalence implies equivalence, but the contrary does not hold. For example,
${\ensuremath{\mathbf{F}}} a \wedge {\ensuremath{\mathbf{G}}} a$ and ${\ensuremath{\mathbf{G}}} a$ are equivalent, but not propositionally equivalent. 

The states of the LDBA for an LTL formula are equivalence classes of formulas (or tuples thereof) 
with respect to propositional equivalence. However, we abuse language and write that the 
states are formulas or tuples of formulas.

\paragraph{Translating LTL to LDBA.}

\newcommand{\delta_{\it in}}{\delta_{\it in}}
\newcommand{\mathcal A_{\it in}}{\mathcal A_{\it in}}
\newcommand{\mathcal A_{\it ac}}{\mathcal A_{\it ac}}

Fix a formula $\varphi$.  We describe the LDBA $\mathcal A_\varphi$. We use 
$\varphi = c \vee{\ensuremath{\mathbf{X}}} {\ensuremath{\mathbf{G}}} (a \vee {\ensuremath{\mathbf{F}}} b)$ as running example. We abbreviate
$\psi := (a \vee {\ensuremath{\mathbf{F}}} b)$, and write $\varphi = c \vee {\ensuremath{\mathbf{X}}}{\ensuremath{\mathbf{G}}}\psi$. 
The LDBA $\mathcal A_\varphi$ is shown in Figure \ref{fig:complete}.

\begin{figure}[ht]
	\begin{center}
		\begin{tikzpicture}[x=2cm,y=1.5cm,font=\footnotesize,initial text=,outer sep=0.5mm]
		
		\node[state,initial] (a) at (0,0) {$\varphi$};
		\node[state] (b) at (0,-1) {${\ensuremath{\mathbf{G}}}\psi$};
		\node[state] (c) at (0,-2) {${\ensuremath{\mathbf{G}}}\psi \wedge {\ensuremath{\mathbf{F}}} b$};
		
		\node[state] (d) at (1.7,0) {${\ensuremath{\mathbf{tt}}}$};
		\node[state] (1c) at (1.7,-1) {$\langle c, \cdot \rangle$};
		\draw node at (3.4,-1) {\textcolor{red}{$\Large c$}};
		\node[state] (1t) at (1.7,-2) {$\langle {\ensuremath{\mathbf{tt}}}, \cdot \rangle$};
		\draw node at (3.4,-2) {\textcolor{red}{$\Large {\ensuremath{\mathbf{tt}}}$}};
		
		\node[state] (1F) at (0,-3) {$\langle {\ensuremath{\mathbf{F}}} b, (\psi, {\ensuremath{\mathbf{tt}}}) \rangle$};
		\draw node at (-1.6,-3) {\textcolor{red}{$\Large {\ensuremath{\mathbf{G}}}\psi \wedge {\ensuremath{\mathbf{F}}} b$}};
		\node[state] (2F) at (0,-4) {$\langle {\ensuremath{\mathbf{F}}} b, ({\ensuremath{\mathbf{F}}} b, \psi) \rangle$};
		\draw node at (-1.6,-4) {\textcolor{red}{$\Large {\ensuremath{\mathbf{G}}}\psi \wedge {\ensuremath{\mathbf{F}}} b$}};
		\node[state] (3F) at (0,-5) {$\langle {\ensuremath{\mathbf{F}}} b, ({\ensuremath{\mathbf{F}}} b, {\ensuremath{\mathbf{F}}} b) \rangle$};
		\draw node at (-1.6,-5) {\textcolor{red}{$\Large {\ensuremath{\mathbf{G}}}\psi \wedge {\ensuremath{\mathbf{F}}} b$}};
		
		\node[state] (1) at (1.7,-3)      {$\langle {\ensuremath{\mathbf{tt}}}, (\psi, {\ensuremath{\mathbf{tt}}}) \rangle$};
		\draw node at (3.4,-3) {\textcolor{red}{$\Large {\ensuremath{\mathbf{G}}}\psi \wedge \psi$}};
		\node[state] (2) at (1.7,-4)     {$\langle {\ensuremath{\mathbf{tt}}}, ({\ensuremath{\mathbf{F}}} b, \psi) \rangle$};
		\draw node at (3.4,-4) {\textcolor{red}{$\Large {\ensuremath{\mathbf{G}}}\psi \wedge {\ensuremath{\mathbf{F}}} b$}};
		\node[state] (3) at (1.7,-5)     {$\langle {\ensuremath{\mathbf{tt}}}, ({\ensuremath{\mathbf{F}}} b, {\ensuremath{\mathbf{F}}} b) \rangle$};
		\draw node at (3.4,-5) {\textcolor{red}{$\Large {\ensuremath{\mathbf{G}}}\psi \wedge {\ensuremath{\mathbf{F}}} b$}};
		
		\draw[dashed] (-1.0,-2.35) -- (0.75, -2.35) -- (0.75, -0.60) -- (3.3, -0.60);
		
		\path[->]
		(a) edge node[left] {$\bar{c}$} (b)
		edge node[above] {$c$} (d)
		edge node[above] {$\epsilon$} (1c)
		edge node[above] {$\epsilon$} (1)
		(b) edge [loop right, max distance=6mm,in=165,out=195,looseness=15] node[left] {$a+b$} (b)
		edge [bend right=-30] node[left]{$\bar{a}\bar{b}$} (c)
		edge node[above]{$\epsilon$} (1)
		(c) edge [bend left=30]  node[left] {$b$} (b)
		edge node[right]{$\epsilon$} (1F)
		edge [loop left,max distance=6mm,in=165,out=195,looseness=15] node[left]{$\bar{b}$} (c)
		(d)  edge [loop left, max distance=6mm,in=20,out=340,looseness=15] node[right] {${\ensuremath{\mathbf{tt}}}$} (d)
		edge [bend left=60] node[right] {$\epsilon$} (1t)
		edge [bend left=75] node[right] {$\epsilon$} (1);
		
		
		\path[->] (1F) edge node[right]{$\bar{a}\bar{b}$} (2F)
		edge node[below]{$b$} (1)
		edge [loop left, max distance=6mm,in=165,out=195,looseness=15] node[left]{$a\bar{b}$} (1F)
		(2F) edge node[right] {$\bar{a}\bar{b}$} (3F)
		edge node[below] {$b$} (1)
		edge  [loop left, max distance=6mm,in=165,out=195,looseness=15] node[left]{$a\bar{b}$} (2F)
		(3F) edge [loop below, max distance=6mm,in=250,out=290,looseness=15] node[below]{$\bar{b}$} (3F)
		edge node[below]{$b$} (1);
		
		\path[->] (1) edge node[right]{$\bar{a}\bar{b}$} (2)
		edge [loop right, max distance=9mm,in=60,out=90,looseness=5, double] node[right]{$a + b$} (1)
		(2) edge node[right] {$\bar{a}\bar{b}$} (3)
		edge[bend left=-60, double] node[right] {$b$} (1)
		edge  [loop right, max distance=4mm,in=340,out=20,looseness=15]node[right]{$a\bar{b}$} (2)
		(3) edge [loop below, max distance=6mm,in=250,out=290,looseness=15] node[below]{$\bar{b}$} (3)
		edge [bend left=-90, double] node[right]{$b$} (1);
		
		\path[->] (1c) edge node[right]{$c$} (1t)
		(1t) edge [loop right, max distance=6mm,in=340,out=20,looseness=15, double] node[right] {${\ensuremath{\mathbf{tt}}}$} (1t);
		
		\end{tikzpicture}
	\end{center}
	\caption{Automaton $\mathcal{A}$ for $\varphi = c \vee {\ensuremath{\mathbf{X}}} {\ensuremath{\mathbf{G}}} (a \vee {\ensuremath{\mathbf{F}}} b)$. The initial component is above the dashed line, the accepting component below.}
	\label{fig:complete}
\end{figure}

The LDBA $\mathcal A_\varphi$ consists of two deterministic components, called the {\em initial} and {\em accepting} 
components, and denoted $\mathcal A_{\it in}$ and $\mathcal A_{\it ac}$, respectively---in Figure \ref{fig:complete} they 
are shown above and below the dashed line. The accepting component $\mathcal A_{\it ac}$ is the union 
(defined componentwise for states, transitions, and accepting states) of subcomponents 
$\mathcal A_\mathcal{G}$, one for each set $\mathcal{G}$ of ${\ensuremath{\mathbf{G}}}$-subformulas of $\varphi$--that is, if $\varphi$
has $n$ different ${\ensuremath{\mathbf{G}}}$-subformulas, then $\mathcal A_{\it ac}$ is the union of $2^n$ subcomponents). 
Transitions of $\mathcal A_\varphi$ labeled by an alphabet letter connect either two states 
of $\mathcal A_{\it in}$, or two states of the same subcomponent of $\mathcal A_{\it ac}$. 
Further, for each state $q$ of $\mathcal A_{\it in}$ and each set $\mathcal{G}$ there is an $\epsilon$-transition 
leading from $q$ to a state of $\mathcal A_\mathcal{G}$. 

\medskip

\noindent {\bf Initial component $\mathcal A_{\it in}$:} Define the set of formulas {\em reachable} from $\varphi$ as 
${\it Reach}(\varphi)~=~\{\psi \mid \exists w. ~ \psi = {\it af}(\varphi,w)\}$. The set of states of $\mathcal A_{\it in}$  is ${\it Reach}(\varphi)$. 
The initial state is $\varphi$. The transition function $\delta_{\it in}$ is given by 
$\delta_{\it in}(\psi, a) = {\it af}(\psi, a)$. 
Intuitively, $\mathcal A_{\it in}$ monitors the formula that has to hold at the current moment for
$\varphi$ to hold at the beginning.

\medskip

\noindent {\bf Accepting component $\mathcal A_{\it ac}$:} The accepting component $\mathcal A_{\it ac}$ 
is the union of subcomponents $\mathcal A_\mathcal{G}$, one for each $\mathcal{G} \subseteq {\ensuremath{\mathbb{G}}}(\varphi)$.

Let ${\ensuremath{\mathbb{G}}}(\varphi)$ denote the set of all ${\ensuremath{\mathbf{G}}}$-subformulas of $\varphi$. 
Given a set $\mathcal{G} \subseteq {\ensuremath{\mathbb{G}}}(\varphi)$ and a formula $\psi$, we write $\psi[\mathcal{G}]$ as an abbreviation
for $\psi[\mathcal{G}, {\ensuremath{\mathbb{G}}}(\varphi) \setminus \mathcal{G}]$, i.e., for the 
result of substituting ${\ensuremath{\mathbf{tt}}}$ for each maximal occurrence of a formula of $\mathcal{G}$ in $\psi$,
and ${\ensuremath{\mathbf{ff}}}$ for each maximal occurrence of a formula of ${\ensuremath{\mathbb{G}}}(\varphi) \setminus \mathcal{G}$ in $\psi$.
For example, if $\mathcal{G} = \{{\ensuremath{\mathbf{G}}}(a \vee {\ensuremath{\mathbf{G}}} b)\}$ then ${\ensuremath{\mathbf{G}}} b \vee {\ensuremath{\mathbf{X}}} (a \wedge {\ensuremath{\mathbf{G}}}(a \vee {\ensuremath{\mathbf{G}}} b))[\mathcal{G}] = {\ensuremath{\mathbf{ff}}} \vee 
{\ensuremath{\mathbf{X}}} (a \wedge {\ensuremath{\mathbf{tt}}}) \equiv {\ensuremath{\mathbf{X}}} a$. 

Each subcomponent $\mathcal A_\mathcal{G}$ is a product of DBAs: One for the formula $\varphi[\mathcal{G}]$, and one for each  
formula of the form ${\ensuremath{\mathbf{G}}}(\psi[\mathcal{G}])$, where ${\ensuremath{\mathbf{G}}}\psi \in \mathcal{G}$. Observe that $\varphi[\mathcal{G}]$ is a ${\ensuremath{\mathbf{G}}}$-free formula,
and ${\ensuremath{\mathbf{G}}}(\psi[\mathcal{G}])$ does not have nested ${\ensuremath{\mathbf{G}}}$s. For example, if $\mathcal{G} = \{ {\ensuremath{\mathbf{G}}} (a \vee {\ensuremath{\mathbf{G}}} b)\}$, then $\mathcal A_\mathcal{G}$ is the
 product of three DBAs, one for $\varphi[\mathcal{G}]$, one for ${\ensuremath{\mathbf{G}}} (b [\mathcal{G}]) = {\ensuremath{\mathbf{G}}} b$, and a third one for ${\ensuremath{\mathbf{G}}} ((a \vee {\ensuremath{\mathbf{G}}} b)[\mathcal{G}]) = {\ensuremath{\mathbf{G}}} (a \vee {\ensuremath{\mathbf{ff}}}) \equiv_P {\ensuremath{\mathbf{G}}} a$. We call the DBAs for $\varphi[\mathcal{G}]$ and ${\ensuremath{\mathbf{G}}}(\psi[\mathcal{G}])$ the 
{\em monitors}. 

\medskip

\noindent {\bf Monitor for $\varphi[\mathcal{G}]$.} The set of states is ${\it Reach}(\varphi[\mathcal{G}])$, the transition function $\delta_{\varphi[\mathcal{G}]}$ is given by $\delta_{\varphi[\mathcal{G}]}(\psi, a) = {\it af}(\psi, a)$. The only final state is ${\ensuremath{\mathbf{tt}}}$.
The initial state is left unspecified. 

\begin{itemize}
\item[$\star$] Lemma 2 of \cite{DBLP:conf/cav/SickertEJK16} shows that the 
$\varphi[\mathcal{G}]$-monitor accepts a word $w$ from a state $q$ 
if{}f $w$ satisfies the formula $q$.
\end{itemize}

\noindent {\bf Monitor for ${\ensuremath{\mathbf{G}}} (\psi[\mathcal{G}]$).} Let us abbreviate $\psi[\mathcal{G}]$ as $\psi'$. The monitor for ${\ensuremath{\mathbf{G}}}\psi'$
is the DBA $\mathcal{U}({\ensuremath{\mathbf{G}}}\psi') = (2^{Ap}, {\it Reach}(\psi') \times {\it Reach}(\psi'), \delta, (\psi', {\ensuremath{\mathbf{tt}}}), F)$ where
\begin{itemize}
	\item $\delta(\, (\xi_1, \xi_2) \, , \nu) = \begin{cases} (\, {\it af}(\xi_2, \nu) \wedge \psi' \, , \, {\ensuremath{\mathbf{tt}}} \, ) & \text{if } {\it af}(\xi_1, \nu) \equiv_P {\ensuremath{\mathbf{tt}}} \\[0.1cm] (\, {\it af}(\xi_1, \nu) \, , \, {\it af}(\xi_2, \nu) \wedge \psi' \, ) & \text{otherwise} \end{cases}$ \\[0.1cm]
	\item $F = \{(\, (\xi_1, \xi_2) \, , \nu, p) \in Q \times 2^{Ap} \times Q \mid {\it af}(\xi_1, \nu) \equiv_P {\ensuremath{\mathbf{tt}}}\}$
\end{itemize}

\begin{itemize}
\item[$\star$] Lemma 5 of \cite{DBLP:conf/cav/SickertEJK16} proves that $\mathcal{U}({\ensuremath{\mathbf{G}}}\psi')$ accepts a word $w$ (from its initial state $(\psi', {\ensuremath{\mathbf{tt}}})$) if{}f $w \models {\ensuremath{\mathbf{G}}}\psi'$. 
\end{itemize}

\noindent {\bf Product.} Fix a set $\mathcal{G} = \{ {\ensuremath{\mathbf{G}}}\psi_1, \ldots, {\ensuremath{\mathbf{G}}}\psi_n\} \subseteq {\ensuremath{\mathbb{G}}}$ of ${\ensuremath{\mathbf{G}}}$-subformulas
of $\varphi$. For every index $1 \leq i \leq n$, let $\mathcal{U}_i = (2^{\it Ap},Q_i, \delta_i, q_{0i}, F_i)$ be the 
monitor for ${\ensuremath{\mathbf{G}}}(\psi_i[\mathcal{G}])$. The {\em product} of these monitors is the generalized deterministic B\"uchi automaton 
\[
\mathcal{P}(\mathcal{G}) = 
(\; 2^{Ap} , 
 \; \prod_{i=1}^n Q_i , 
 \; \prod_{i=1}^n \delta_i , 
 \; (q_{01}, \ldots, q_{0n}) , 
 \; \{F_1', \ldots, F_n'\} \; )
\] 
where $( \; (q_1, \ldots, q_n), \nu, (q, q_1', \ldots, q_n') \; )$ is  a transition of 
$F_i'$ if{}f $(q_i, \nu, q_i') \in F_i$.

\begin{itemize}
\item[$\star$] Lemma 5 of \cite{DBLP:conf/cav/SickertEJK16} proves that $\mathcal{P}(\mathcal{G})$ 
accepts $w$ if{}f $w \models {\ensuremath{\mathbf{G}}}(\psi[\mathcal{G}])$ for all ${\ensuremath{\mathbf{G}}}\psi \in \mathcal{G}$.
\end{itemize}

\noindent {\bf Subcomponent $\mathcal A_\mathcal{G}$}. The subcomponent is the product of the monitor
for $\varphi[\mathcal{G}]$ and $\mathcal{P}(\mathcal{G})$:
\[\mathcal A_\mathcal{G}  = (\; 2^{Ap} \; , \; {\it Reach}(\varphi[\mathcal{G}]) \times \prod_{i=1}^n Q_i \; , \; \delta_{\varphi[\mathcal{G}]} \times \prod_{i=1}^n \delta_i \; , \; \{ \{ \tt \} \times F_1', \ldots, \{ \tt \} \times F_n'\} \; )\]

\begin{itemize}
\item[$\star$] We have: $\mathcal A_\mathcal{G}$ accepts a word $w$ from the state $(\varphi'[\mathcal{G}], q_{01}, \ldots, q_{0n})$ 
if{}f $w \models \varphi'[\mathcal{G}] \wedge {\ensuremath{\mathbf{G}}}(\psi[\mathcal{G}])$.
\end{itemize}

\noindent {\bf Connecting $\epsilon$-transitions:} Finally, we describe the $\epsilon$-transitions connecting 
the initial component $\mathcal A_{\it in}$ to the accepting component $\mathcal A_{\it ac}$.
There is an $\epsilon$-transition for each state $\varphi'$ of $\mathcal A_{\it in}$ and
each set $\mathcal{G}= \{ {\ensuremath{\mathbf{G}}}\psi_1, \ldots, {\ensuremath{\mathbf{G}}}\psi_n\} \subseteq {\ensuremath{\mathbb{G}}}(\varphi)$. The transition is 
$\big(\varphi', \epsilon, (\, \varphi'[\mathcal{G}], {\ensuremath{\mathbf{G}}}(\psi_1[\mathcal{G}]), \ldots, {\ensuremath{\mathbf{G}}}(\psi_n[\mathcal{G}])\,)\big)$.
\begin{itemize}
\item[$\star$] {\bf Theorem 1} of \cite{DBLP:conf/cav/SickertEJK16} proves that $w \models \varphi$ if{}f  $\mathcal A_\varphi$ accepts $w$. 
\end{itemize}
\noindent This concludes the description of $\mathcal A_\varphi$.

\paragraph{Proof of Proposition \ref{prop:translation}.}

We start by generalizing Lemma 5 of \cite{DBLP:conf/cav/SickertEJK16} as follows:

\begin{lemma} \label{lem:prodcorrect2}
$\mathcal{U}({\ensuremath{\mathbf{G}}}\psi')$ accepts a word $w$ from a state $(\xi_1, \xi_2)$ if{}f 
$w \models {\ensuremath{\mathbf{G}}}\psi' \wedge \xi_1 \wedge \xi_2$.
\end{lemma}
\begin{proof}
We first claim that there is a formula $\xi$ such that $\xi_1 \wedge \xi_2 \equiv \xi \wedge \psi'$.
If $(\xi_1, \xi_2)=(\psi', {\ensuremath{\mathbf{tt}}})$, then $\xi = {\ensuremath{\mathbf{tt}}}$.
Otherwise there is $(\xi_1', \xi_2')$ and $\nu$ such that $\delta((\xi_1', \xi_2'), \nu) = (\xi_1, \xi_2)$. 
By the definition of the transition function, either $\xi_1 = \eta_1 \wedge \psi'$ for some $\eta_1$,
or $\xi_2 = \eta_2 \wedge \psi'$ for some $\eta_2$, and we can choose $\xi$ accordingly.

By this result, we have ${\it af}(\xi_1 \wedge \xi_2, \nu) \equiv {\it af}(\xi \wedge \psi', \nu) \equiv {\it af}(\xi, \nu) \wedge {\it af}(\psi', \nu)$ for every state $(\xi_1, \xi_2)$ and letter $\nu$, and so in particular
\begin{equation}
\label{eq1}
{\it af}(\xi_1, \nu) \wedge {\it af}(\xi_2, \nu) \models {\it af}(\psi', \nu)
\end{equation}

We now prove the lemma. Let $v$ be a finite word leading from the initial state $(\psi', {\ensuremath{\mathbf{tt}}})$ to $(\xi_1, \xi_2)$. We proceed by induction of the length of $v$.

\noindent {\bf Basis.}  $v = \epsilon$. Then $(\xi_1, \xi_2) = (\psi', {\ensuremath{\mathbf{tt}}})$, and so $w \models {\ensuremath{\mathbf{G}}}\psi' \wedge \xi_1 \wedge \xi_2$
if{}f $w \models {\ensuremath{\mathbf{G}}}\psi' \wedge \psi' \equiv {\ensuremath{\mathbf{G}}}\psi'$. By Lemma 5 of \cite{DBLP:conf/cav/SickertEJK16} $w \models {\ensuremath{\mathbf{G}}}\psi'$
if{}f $\mathcal{U}({\ensuremath{\mathbf{G}}}\psi')$ accepts $w$ from $(\psi', {\ensuremath{\mathbf{tt}}})$, and we are done.

\noindent {\bf Step.} $v = v' \nu$ for some word $v'$ and letter $\nu$. Then there is a state $(\xi_i', \xi_2')$ 
such that $\delta((\psi', {\ensuremath{\mathbf{tt}}}), v')= (\xi_1', \xi_2')$ and $\delta((\xi_1', \xi_2'), v')= (\xi_1, \xi_2)$.
By induction hypothesis a word $w$ is accepted from $(\xi_1', \xi_2')$ if{}f 
$w \models {\ensuremath{\mathbf{G}}}\psi' \wedge \xi_1' \wedge \xi_2'$.
We consider two cases.

If ${\it af}(\xi_1', \nu) \equiv_P  {\ensuremath{\mathbf{tt}}}$, then by the definition of $\delta$ we have 
 $\delta((\xi_1', \xi_2'), \nu) = ({\it af}(\xi_2', \nu) \wedge \psi', {\ensuremath{\mathbf{tt}}})$. It follows:

\begin{center}
\begin{tabular}{cl}
       & $\mathcal{U}({\ensuremath{\mathbf{G}}}\psi')$ accepts $w$ from $(\xi_1, \xi_2)$ \\
  if{}f & (determinism) \\
       & $\mathcal{U}({\ensuremath{\mathbf{G}}}\psi')$ accepts $\nu w$ from $(\xi_1', \xi_2')$ \\
  if{}f & (induction hypothesis) \\
       & $\nu w \models {\ensuremath{\mathbf{G}}}\psi' \wedge \xi_1' \wedge \xi_2'$ \\
  if{}f & (fundamental property of ${\it af}$) \\
       & $w \models {\it af}(\, {\ensuremath{\mathbf{G}}}\psi' \wedge \xi_1' \wedge \xi_2' \, , \, \nu)$ \\
  if{}f & (definition of ${\it af}$) \\
       & $w \models {\ensuremath{\mathbf{G}}}\psi' \wedge {\it af}(\psi' \nu) \wedge {\it af}(\xi_1', \nu) \wedge {\it af}(\xi_2', \nu)$ \\
  if{}f & (Equation \ref{eq1}) \\
       & $w \models {\ensuremath{\mathbf{G}}}\psi' \wedge {\it af}(\xi_1', \nu) \wedge {\it af}(\xi_2', \nu)$ 
\end{tabular}
\end{center}

We conclude the proof by showing
${\ensuremath{\mathbf{G}}}\psi' \wedge {\it af}(\xi_1', \nu) \wedge {\it af}(\xi_2', \nu) \equiv {\ensuremath{\mathbf{G}}}\psi' \wedge \xi_1 \wedge \xi_2$.
It suffices to prove $\xi_1 \wedge \xi_2 \equiv {\it af}(\xi_1', \nu) \wedge {\it af}(\xi_2', \nu) \wedge \psi'$.
Consider two cases:
\begin{itemize}
\item ${\it af}(\xi_1', \nu) \equiv_P {\ensuremath{\mathbf{tt}}}$. Then, by the definition of $\mathcal{U}({\ensuremath{\mathbf{G}}}\psi')$, we have
$\xi_1 = {\it af}(\xi_2', \nu) \wedge \psi'$ and $\xi_2 = {\ensuremath{\mathbf{tt}}}$, and we are done.
\item ${\it af}(\xi_1', \nu) \not\equiv_P {\ensuremath{\mathbf{tt}}}$. Then,by the definition of $\mathcal{U}({\ensuremath{\mathbf{G}}}\psi')$, we have
$\xi_1 = {\it af}(\xi_1', \nu)$ and $\xi_2 = {\it af}(\xi_1', \nu) \wedge \psi'$, and we are done. \qed
\end{itemize}
\end{proof}

We can now proceed to prove Proposition \ref{prop:translation}.

\begin{refproposition}{prop:translation}
For every LTL formula $\varphi$, every state $s$ of the LDBA of \cite{DBLP:conf/cav/SickertEJK16} for $\varphi$ can be labelled by an LTL formula $\mathit{label}(s)$ such that (i) $\mathsf{L}(s)=\mathsf{L}(\mathit{label}(s))$ and (ii) $\mathit{label}(s)$ is a Boolean combination of subformulas of $\varphi[T_s, F_s]$ for some $T_s$ and $F_s$. Moreover, the LDBA is initial-deterministic.

Further, $\mathit{label}(s)$ can be computed in linear time from the descriptor of $s$.
\end{refproposition}
\begin{proof}
Recall the two properties of the ${\it af}$ function.
For every formula $\varphi$, finite word $v$, and $\omega$-word $w$:
\begin{itemize}
\item[(i)]  $vw \models \varphi$ if{}f $w \models {\it af}(\varphi,v)$.
\item[(ii)]  ${\it af}(\varphi, v)$ is a boolean combination of subformulas of $\varphi$.
Therefore, every formula of ${\it Reach}(\varphi)$ is a boolean combination of subformulas of $\varphi$.
\end{itemize}

Let $s$ be a state of $\mathcal A_{\it in}$, and let $v$ be any finite 
word leading from $s_0$ to $s$. By Theorem 1 of \cite{DBLP:conf/cav/SickertEJK16}, we have $L(s_0) = L(\varphi)$. 
By (i), $\mathsf{L}({\it af}(\varphi,v)) = \{w \mid vw \in \mathsf{L}(\varphi) \}$. Since $\mathcal A_{\it in}$ is deterministic, 
$\mathsf{L}(s) = \{w \mid vw \in \mathsf{L}(s_0) \} = \{w \mid vw \in \mathsf{L}(\varphi) \} = \mathsf{L}({\it af}(\varphi,v))$.
So we can take $\mathit{label}(s) = s$.

We consider now the case that $s$ belongs to $\mathcal A_{\it ac}$. Then there is a set $\mathcal{G}=({\ensuremath{\mathbf{G}}}\psi_1, \ldots, {\ensuremath{\mathbf{G}}}\psi_n)$
such that $s$ belongs to $\mathcal A_\mathcal{G}$. By the definition of $\mathcal A_\mathcal{G}$ as product of DBAs,
$s$ is of the form $(\varphi'[\mathcal{G}], (\xi_{11}, \xi_{21}), \ldots, (\xi_{1n}, \xi_{2n}))$,
where $\varphi'[\mathcal{G}]$ is a state of the monitor for $\varphi[\mathcal{G}]$, and $(\xi_{1i}, \xi_{2i})$ is a state of the 
monitor for ${\ensuremath{\mathbf{G}}}(\psi_i[\mathcal{G}])$.  Further, the words recognized from $s$ are those simultaneously
recognized from $\varphi'[\mathcal{G}]$, $(\xi_{11}, \xi_{21}), \ldots, (\xi_{1n}, \xi_{2n})$ in their respective automata. 
By Lemma \ref{lem:prodcorrect2}, the words recognized from $s$ are those satisfying 
$\varphi'[\mathcal{G}] \wedge \xi_{11} \wedge \xi_{21} \wedge \ldots \wedge \xi_{1n} \wedge \xi_{2n}$.
We choose $\mathit{label}(s)$ as this formula. 
It remains to show that each conjunct of $\mathit{label}(s)$ is a boolean combination of formulas of $\mathsf{sf}(\varphi)[\mathcal{G}]$.

\begin{itemize}
\item By the definition of the monitor for $\varphi[\mathcal{G}]$, the formula $\varphi'[\mathcal{G}]$ belongs to 
${\it Reach}(\varphi[\mathcal{G}])$, and by (ii) we are done.
\item By the definition of the monitor for ${\ensuremath{\mathbf{G}}}(\psi_i[\mathcal{G}])$, the formulas $\xi_{1i}$ and $\xi_{2i}$ belong to 
${\it Reach}(\psi_i[\mathcal{G}])$. By (ii), they are boolean combinations of subformulas of $\psi_i[\mathcal{G}]$.
Since $\psi_i$ is a subformula of $\varphi$, they are also boolean combinations of subformulas of 
$\varphi[\mathcal{G}]$, and so a boolean combination of formulas of $\mathsf{sf}(\varphi)[\mathcal{G}]$. \qed
\end{itemize}
\end{proof}

\iffalse
\section{Example}

\begin{example}
	Consider the LDBA for ${\ensuremath{\mathbf{G}}}{\ensuremath{\mathbf{F}}} a$ in Fig.~\ref{fig:ex-ltl-redundant}. 
	It has the following states: ${\ensuremath{\mathbf{G}}}{\ensuremath{\mathbf{F}}} a, f:=({\ensuremath{\mathbf{ff}}}, {\ensuremath{\mathbf{tt}}}, {\ensuremath{\mathbf{tt}}}), t_1:=({\ensuremath{\mathbf{tt}}},{\ensuremath{\mathbf{F}}} a,{\ensuremath{\mathbf{tt}}}), t_2:=({\ensuremath{\mathbf{tt}}},{\ensuremath{\mathbf{F}}} a,{\ensuremath{\mathbf{F}}} a)$.
	In the dag of the word $\emptyset^\omega$, ${\ensuremath{\mathbf{G}}}{\ensuremath{\mathbf{F}}} a$ in each step spawns $t_1$.
	Additionally, since older $t_1$'s have meanwhile changed to $t_2$, eventually we have ${\sf Ind}(t_2)=1$ and also ${\sf Ind}(t_1)=2$.
	However, spawning new $t_1$'s is useless as $\mathsf{L}(t_1)=\mathsf{L}(t_2)=\mathsf{L}({\ensuremath{\mathbf{F}}} a\wedge {\ensuremath{\mathbf{G}}}{\ensuremath{\mathbf{F}}} a)$.
	Indeed, adding a new state $t_1$ recognizing the same language is not necessary and we can continue the breakpoint process for the older $t_2$.
	\begin{figure}
		\includegraphics[scale=0.3]{ltl-redundant}
		\caption{An example of redundant nodes in the dag}
		\label{fig:ex-ltl-redundant}
	\end{figure}
\end{example}

\fi


\section{Conclusion}

We have presented a simple, \enquote{Safraless}, and asymptotically optimal  translation from LTL and LDBA to deterministic parity automata. 
Furthermore, the translation is suitable for an on-the-fly implementation. The resulting automata are substantially smaller
than those produced by the SPOT library for formulas obtained from synthesis specifications, and have comparable or smaller size
for other benchmarks. In future work we want to investigate the performance of the translation as part of a synthesis toolchain.

\paragraph{Acknowledgments.} The authors want to thank Michael Luttenberger for helpful discussions and the anonymous reviewers for constructive feedback.



\section{Experimental Evaluation}

We evaluate the performance of our construction on several datasets taken from 
\cite{DBLP:conf/lpar/BlahoudekKS13,DeWulf:2008vt,DBLP:conf/cav/SickertEJK16} and several Temporal 
Logic Synthesis Format (TLSF) specifications \cite{DBLP:journals/corr/JacobsBBK0KKLNP16} of
the SyntComp 2016 competition. 

We use the size of the constructed deterministic automaton as an indicator 
for the overall performance of the synthesis procedure. In \cite{DBLP:conf/charme/SebastianiT03} 
it is argued that the degree of determinism of the automaton is a better predictor for performance
in model-checking problems; however, this parameter is not applicable for synthesis problems, which
require deterministic automata. 

We compare two versions of our implementation (with and without optimizations, see below)
with the algorithms of Spot \cite{duret.16.atva2}. Each tool is given 64GB
of memory and 10 minutes. Increasing time to 10 hours
does not change the results. More precisely, we compare the following three setups:

\medskip \noindent \textbf{S.} (\texttt{ltl2tgba}, 2.1.1) - Spot \cite{duret.16.atva2} implements a
version of the Safra-Piterman determinization procedure \cite{DBLP:journals/fuin/Redziejowski12}
with several optimizations.

\medskip \noindent \textbf{L2P and L2P$'$.}  (\texttt{ltl2dpa}, 1.0.0) - L2P is the construction of this paper,
available at \url{www7.in.tum.de/~sickert/projects/ltl2dpa}. 
L2P$'$ adds two optimizations. First, the tool translates both the formula and its negation to 
DPAs $A_1, A_2$, complements $A_2$ to yield $\overline{A}_2$, and picks the smaller of $A_1, A_2$. 
Further, we apply the simplification routines of Spot (\texttt{ltlfilt} and \texttt{autfilt}, respectively). 

\begin{figure}[t]
	\vspace*{-2cm}
	\input{exp1}
	\caption{Comparison of Spot and our implementation using the best configurations. Timeouts are denoted by setting the size of the automaton to the maximum.}
        \label{fig:scatter}
	
	\medskip
	

	\captionof{table}{Number of states and number of used colours in parenthesis for the constructed automata. Timeouts are marked with $t$.}
	\label{tab:exp}
	\input{exp2}

	\vspace*{-1em}\myspace
\end{figure}

\medskip

We consider three groups of benachmarks:

\medskip

\noindent \textbf{Parametric Formulas.}
10 benchmarks from  \cite{DBLP:conf/lpar/BlahoudekKS13,DBLP:conf/cav/SickertEJK16}).
In six cases S and L2P$'$ produce identical results. The other four are
\[\begin{array}{rlrl}
R(n) & = \ensuremath{\bigwedge_{i=1}^n} ({\ensuremath{\mathbf{G}}}{\ensuremath{\mathbf{F}}} p_i \vee {\ensuremath{\mathbf{F}}}{\ensuremath{\mathbf{G}}} p_{i+1}) & G(n) & = (\ensuremath{\bigwedge_{i=1}^n} {\ensuremath{\mathbf{G}}}{\ensuremath{\mathbf{F}}} p_i) \rightarrow (\ensuremath{\bigwedge_{i=1}^n} {\ensuremath{\mathbf{G}}}{\ensuremath{\mathbf{F}}} q_i) \\
\theta(n) & = \neg ((\ensuremath{\bigwedge_{i=1}^n} {\ensuremath{\mathbf{G}}} {\ensuremath{\mathbf{F}}} p_i) \rightarrow {\ensuremath{\mathbf{G}}}(q \rightarrow {\ensuremath{\mathbf{F}}} r)) & F(n) & = \ensuremath{\bigwedge_{i=1}^n} ({\ensuremath{\mathbf{G}}}{\ensuremath{\mathbf{F}}} p_i \rightarrow {\ensuremath{\mathbf{G}}}{\ensuremath{\mathbf{F}}} q_i) \\
\end{array}\]
\noindent for which the results are shown in (figure \ref{fig:scatter}a). Additionally, we consider the 
``$f$'' formulas from \cite{DBLP:conf/cav/SickertEJK16} (table \ref{tab:exp}). 
Observe that L2P$'$ performs clearly better, and the gap between the tools grows when the parameter increases. 

\medskip \noindent \textbf{Randomly Generated Formulas} from \cite{DBLP:conf/lpar/BlahoudekKS13} (figure \ref{fig:scatter}b). 

\medskip \noindent \textbf{Real Data.} Formulas taken from case studies and synthesis competitions --- the intended domain of application of our approach. Figures \ref{fig:real} and \ref{fig:acacia} show results for 
the real-world formulas of \cite{DBLP:conf/lpar/BlahoudekKS13} and the TLSF specifications contained in the Acacia set of \cite{DBLP:journals/corr/JacobsBBK0KKLNP16}. Table \ref{tab:exp} shows results for LTL formulas expressing properties of
Szymanski's protocol \cite{DeWulf:2008vt}, and for the generalised buffer benchmark of Acacia.

\medskip \noindent \textbf{Average Compression Ratios.}  The geometric average compression ratio for a benchmark suite $B$ 
is defined as ${\prod_{\varphi \in B}  (n_\varphi^S / n^{L2P'}_\varphi)}^{1/|B|}$, 
where $n_\varphi^S$ and $n^{L2P'}_\varphi $ denote the number of states of the automata produced 
by Spot and L2P$'$, respectively. The ratios in our experiments (excluding benchmarks where Spot times out)
are: 1.14 for random formulas, 1.12 for the real-world formulas of \cite{DBLP:conf/lpar/BlahoudekKS13},
and 1.35 for the formulas of Acacia.

\section{Introduction}

Limit-deterministic Büchi automata (LDBA, also known as semi-deterministic Büchi automata) were introduced by Courcoubetis and Yannakakis (based on previous work by Vardi) to solve the 
qualitative probabilistic model-checking problem: Decide if the executions of a Markov chain or Markov Decision Process satisfy a given LTL formula with probability 1 \cite{DBLP:conf/focs/Vardi85,DBLP:conf/lics/VardiW86,DBLP:journals/jacm/CourcoubetisY95}. The problem faced by these authors was that fully nondeterministic Büchi automata (NBAs), which are as expressible as LTL, and more, cannot be used for probabilistic model checking, and deterministic Büchi automata (DBA) are less expressive than LTL. The solution was to introduce LDBAs as a model in-between: as expressive as NBAs, but deterministic enough.

After these papers, LDBAs received little attention. The alternative path of translating the LTL formula into an equivalent fully deterministic Rabin automaton using Safra's construction \cite{DBLP:conf/focs/Safra88} was considered a better option, mostly because it also solves the quantitative probabilistic model-checking problem (computing the probability of the executions that satisfy a formula). However, recent papers  have shown that LDBAs were unjustly forgotten. Blahoudek {\em et al.} have shown that LDBAs are easy to complement \cite{DBLP:conf/tacas/BlahoudekHSST16}. Kini and Viswanathan have given a single exponential translation of
LTL$_{\setminus{\ensuremath{\mathbf{G}}}{\ensuremath{\mathbf{U}}}}$ to LDBA \cite{DBLP:conf/tacas/KiniV15}. Finally, 
Sickert {\em et al.} describe in \cite{DBLP:conf/cav/SickertEJK16}  a double exponential translation for full LTL that can also be applied to the quantitative case, and behaves better than Safra's construction in practice.

In this paper we add to this trend by showing that LDBAs are also attractive for synthesis. The standard solution to the synthesis problem with LTL objectives consists of translating the LTL formula into a deterministic parity automaton (DPA) with the help of the Safra-Piterman construction \cite{DBLP:journals/lmcs/Piterman07}. While limit-determinism is not ``deterministic enough'' for the synthesis problem, we introduce a conceptually simple and worst-case optimal translation LDBA$\rightarrow$DPA. Our translation bears some similarities with that of \cite{bernd} where, 
however, a Muller acceptance condition is used. This condition can also be phrased as a Rabin condition, but not as a parity condition. Moreover, the way of tracking all possible states and finite runs differs.

Together with the translation LTL$\rightarrow$LDBA of \cite{DBLP:conf/cav/SickertEJK16}, our construction provides a \enquote{Safraless}, procedure to obtain a DPA from an LTL formula. However, the direct concatenation of the two constructions does not yield an algorithm of optimal complexity: the LTL$\rightarrow$LDBA translation is double exponential (and there is a double-exponential lower bound), and so for the LTL$\rightarrow$DPA translation we only obtain a triple exponential bound. In the second part of the paper we solve this problem. We show that the LDBAs derived from LTL formulas satisfy a special property, and prove that for such automata the concatenation of the two constructions remains double exponential. To the best of our knowledge, this is the first 
double exponential \enquote{Safraless} LTL$\rightarrow$DPA procedure. (Another asymptotically optimal
\enquote{Safraless} procedure for determinization of B\"uchi automata with Rabin automata as target
has been presented in \cite{DBLP:journals/iandc/FogartyKVW15}.)

In the third and final part, we report on the performance of an 
implementation of our LTL$\rightarrow$LDBA$\rightarrow$DPA construction, and compare it with
algorithms implemented in the SPOT library \cite{duret.16.atva2}. 
Note that it is not possible to force SPOT to always produce DPA, sometimes it produces a deterministic generalized Büchi automaton (DGBA).
The reason is that DGBA are often smaller than DPA (if they exist) and game-solving algorithms for DGBA are not less efficient than for DPA. 
Therefore, also our implementation may produce DGBA in some cases.
We show that our implementation outperforms SPOT for several sets of parametric formulas and formulas used in synthesis examples taken from the SyntComp 2016 competition, and remains competitive  for randomly generated formulas.

\vspace*{-1em}

\paragraph{{\bf Structure of the paper}}
Section~2 introduces the necessary preliminaries about automata. Section~3 defines the translation LDBA$\rightarrow$DPA. Section~4 shows how to compose of LTL$\rightarrow$LDBA  and LDBA$\rightarrow$DPA in such a way that the resulting DPA is at most doubly exponential in the size of the LTL formula. Section~5 reports on the experimental evaluation of this worst-case optimal translation, and Section~6 contains our conclusions.
The paper is a full version of a TACAS'17 paper.

\subsection{Complexity Analysis}

\subsubsection{Upper bound}

Let $n = |Q|$ be the size of the LDBA and let $n_d = |Q_d|$ be the size of the accepting component. We can bound the number of different orderings using the series of reciprocals of factorials (with $e$ being Euler's number):

\[
|{\cal OP}(Q_d)| = \sum_{i=0}^{n_d}\frac{n_d!}{(n_d-i)!} \leq  n_d \cdot n_d!  \cdot \sum_{i=0}^{\infty}\frac{1}{i!} = e \cdot n_d \cdot n_d! \in\mathcal O(2^{n\cdot\log n})
\]

\noindent Thus the obtained DPA has ${\cal O}(2^n\cdot2^{n\cdot\log n}) = 2^{\mathcal O(n\cdot\log n)}$ states and ${\cal O}(n)$ colours

\subsubsection{Lower bound}

We obtain a matching lower bound by strengthening Theorem~8 from \cite{DBLP:conf/fsttcs/Loding99}:


\begin{lemma}
There exists a family $(L_n)_{n \geq 2}$ of languages ($L_n$ over an alphabet of $n$ letters) such that for every $n$ the language $L_n$ can be recognized by a limit-deterministic Büchi automaton with $3n + 2$ states but can not be recognized by a deterministic Parity automaton with less than $n!$ states.
\end{lemma}

\begin{proof}
The proof of Theorem 8 from \cite{DBLP:conf/fsttcs/Loding99} constructs a non-deterministic Büchi automaton of exactly this size and which is in fact limit-deterministic. 

Assume there exists a deterministic Parity automata for $L_n$ with $m < n!$ states. Since parity automata are closed under complementation, we can obtain a parity automaton and hence also a Rabin automaton of size $m$ for $\overline{L_n}$ and thus a Streett automaton of size $m$ for $L_n$, a contradiction to Theorem~8 of \cite{DBLP:conf/fsttcs/Loding99}.\qed
\end{proof}

\begin{corollary}
Every translation from limit-deterministic Büchi automata of size $n$ to deterministic parity yields automata with $2^{\Omega(n \log n)}$ states in the worst case.
\end{corollary}
\subsection{Construction of the DPA}

From an LDBA $A=(Q,Q_d,q_0,\Sigma,\delta,\alpha)$ and an ordering function ${\sf Ord}  : Q \rightarrow \{1,2,\dots,|Q_d|,+\infty\}$ compatible with $Q_d$, we construct a deterministic parity automaton $B=(Q^B,q_0^B,\Sigma,\delta^B,p)$ that, on a word $w$, constructs the levels of the run DAG $G_w$ and the coloring of previous section. Theorem~\ref{thm:coloring} tells us that such an automaton accepts the same language as $A$. 

First, we need some notations. Given a finite set $S$, we note ${\cal P}(S)$ the set of its subsets, and ${\cal OP}(S)$ the set of its totally ordered subsets. So if $(s,<) \in {\cal OP}(S)$ then $s \subseteq S$ and $\mathord{<} \subseteq s \times s$ is a total strict order on $s$. For $e \in s$, we denote by ${\sf Ind}_{(s,<)}(e)$ the position of $e \in s$ among the elements in $s$ for the total strict order $<$, with the convention that the index of the $<$-minimum element is equal to $1$. The deterministic parity automaton $B=(Q^B,q_0^B,\Sigma,\delta^B,p)$ is defined as follows.

\paragraph{{\bf States and initial state}}
The set of states is $Q^B={\cal P}(\overline{Q_d}) \times {\cal OP}(Q_d)$, i.e. a state  of $B$ is a pair $(s,(t,<))$ where $s$ is a set of states outside $Q_d$, and $t$ is an ordered subset of $Q_d$. The ordering reflects the relative index of each state within $t$. The initial state is $q^B_0=(\{q_0\},(\{\},\{\}))$.

\paragraph{{\bf Transition function}}
Let $(s_1,(t_1,<_1))$ be a state in $Q^B$, and $\sigma \in \Sigma$. Then $\delta^B((s_1,(t_1,<_1)))=(s_2,(t_2,<_2))$ where:
		\begin{itemize}
			\item $s_2 = {\sf post}^{\sigma}_{\delta}(s_1) \cap \overline{Q_d}$;
			\item $t_2 =  {\sf post}^{\sigma}_{\delta}(s_1 \cup t_1) \cap Q_d$;
			\item $<_2$ is defined from $<_1$ and ${\sf Ord}$ as follows:
				$\forall q_1,q_2 \in t_2$: $q_1 <_2 q_2$ iff:
			
			  \begin{enumerate}
			  	\item {\bf either}, $\neg\exists q'_1 \in t_1:q_1=\delta(q'_1,\sigma)$, and $\neg\exists q'_2 \in t_1:q_2=\delta(q_2',\sigma)$, and ${\sf Ord}(q_1) < {\sf Ord}(q_2)$,\\
			  	\noindent
			  	i.e. none has a predecessor in $Q_d$, then they are ordered using ${\sf Ord}$;
				
				\item {\bf or}, $\exists q_1' \in t_1: q_1=\delta(q_1',\sigma)$, and $\neg\exists q'_2 \in t_1:q_2=\delta(q_2',\sigma)$,\\
				\noindent i.e. $q_1$ has a $\sigma$-predecessor in $Q_d$, and $q_2$ not;
				
				\item {\bf or} $\exists q'_1 \in t_1:q_1=\delta(q'_1,\sigma)$, and $\exists q'_2 \in t_1:q_2=\delta(q_2',\sigma)$, and $\min_{<_1} \{ q'_1 \in t_1 \mid q_1=\delta(q'_1,\sigma)\} < \min_{<_1} \{ q'_2 \in t_1 \mid q_2=\delta(q'_2,\sigma) \}$,\\
				\noindent
				i.e. both have a predecessor in $Q_d$, and they are ordered according to the order of their minimal parents.
			\end{enumerate}
		\end{itemize}
		
\paragraph{{\bf Coloring}} To define the coloring of edges in the deterministic automaton, we need to identify the states $q \in t_1$ in a transition $(s_1,(t_1,<_1)) \stackrel{\sigma}{\rightarrow} (s_2,(t_2,<_2))$ whose indices decrease when going from $t_1$ to $t_2$. Those are defined as follows:
		\[{\sf Dec}(t_1)= \{ q_1 \in t_1 \mid {\sf Ind}_{(t_2,<_2)}(\delta(q_1,\sigma)) < {\sf Ind}_{(t_1,<_1)}(q_1) \}.\]
\noindent
Additionally, let ${\sf Acc}(t_1)=\{ q \mid \exists q' \in t_2 : (q,\sigma,q') \in  \alpha \}$ denote the subset of states in $t_1$ that are the source of an accepting transition.

We assign a color to each transition $(s_1,(t_1,<_1)) \rightarrow^{\sigma} (s_2,(t_2,<_2))$ as follows:

\begin{enumerate}
	\item if ${\sf Dec}(t_1)=\emptyset$ and ${\sf Acc}(t_1)\not=\emptyset$, the color is $2 \cdot\min_{q \in {\sf Acc}(t_1)} {\sf Ind}_{(t_1,<_1)}(q)$.
	\item if ${\sf Dec}(t_1)\not=\emptyset$ and ${\sf Acc}(t_1)=\emptyset$, the color is $2 \cdot\min_{q \in {\sf Dec}(t_1)} {\sf Ind}_{(t_1,<_1)}(q)-1$.
	\item if ${\sf Dec}(t_1)\not=\emptyset$ and ${\sf Acc}(t_1)\not=\emptyset$, the color is defined as the minimal color among 
		\begin{itemize}
			\item $c_{{\sf odd}}=2 \cdot\min_{q \in {\sf Dec}(t_1)} {\sf Ind}_{(t_1,<_1)}(q)-1$, and 
			\item $c_{{\sf even}}=2 \cdot \min_{q \in {\sf Acc}(t_1)} {\sf Ind}_{(t_1,<_1)}(q)$.
		\end{itemize}
	\item if ${\sf Dec}(t_1)={\sf Acc}(t_1)=\emptyset$, the color is $2 \cdot |Q_q|+1$.
\end{enumerate}

\begin{figure}[t]
\vspace*{-1em}\myspace\vspace*{-1em}
	\begin{center}
		\begin{tikzpicture}
		[x=2cm,y=7mm,font=\small,initial text=,outer sep=0pt]
		
		\node[state,initial] (1) at (0,0) {$\{1\},[]$};
		\node[state] (2) at (1,1) {$\{1\},[2]$}; 
		\node[state] (3) at (1,-1) {$\{1\},[3]$};   	
		\node[state] (4) at (2,1) {$\{1\},[4< 3]$}; 
		\node[state] (5) at (2,-1) {$\{1\},[4< 2]$}; 
		
		\path[->]
		(1) edge[bend left] node[above]{a} node[below]{7}  (2)
		(2) edge[loop above] node[above]{a} node[below]{2} ()
		(1) edge[bend right] node[above]{7} node[below]{b}  (3)
		(3) edge[loop below] node[above]{2} node[below]{b} ()
		(2) edge node[above]{b} node[below]{4}  (4)
		(4) edge[loop above] node[above]{b} node[below]{4} ()
		(3) edge node[above]{4} node[below]{a}  (5)
		(5) edge[loop below] node[above]{4} node[below]{a} ()
		(4) edge[bend left] node[right]{a} node[left]{3}  (5)
		(5) edge[bend left] node[left]{b} node[right]{3}  (4)   	
		;
		\end{tikzpicture}
		~~~
		\begin{tikzpicture}
		[x=2cm,y=7mm,font=\small,initial text=,outer sep=0pt]
		
		\node[state,initial] (1) at (0,0) {$\{1\},[]$};
		\node[state] (2) at (1,1) {$\{1\},[2]$}; 
		\node[state] (3) at (1,-1) {$\{1\},[3]$};   	
		
		\path[->]
		(1) edge[bend left] node[above]{a} node[below]{3}  (2)
		(2) edge[loop above] node[above]{a} node[below]{2} ()
		(1) edge[bend right] node[above]{3} node[below]{b}  (3)
		(3) edge[loop below] node[above]{2} node[below]{b} ()
		(2) edge[bend left] node[right]{a} node[left]{1}  (3)
		(3) edge[bend left] node[left]{b} node[right]{1}  (2)   	
		;
		\end{tikzpicture}
	\end{center}
	\vspace*{-1em}\myspace
	\caption{\label{fig:DPA-ex} Left: DPA that accepts the  LTL language ${\ensuremath{\mathbf{F}}} {\ensuremath{\mathbf{G}}} a \lor {\ensuremath{\mathbf{F}}} {\ensuremath{\mathbf{G}}} b$, edges are decorated with a natural number that specifies its color. Right: A reduced DPA. }
	\vspace*{-1em}
\end{figure}


\begin{example}
The DPA of Fig.~\ref{fig:DPA-ex} is the automaton that is obtained by applying the construction LDBA$\rightarrow$DPA defined above to the LDBA of Fig.~\ref{fig:ex-LDBA} that recognizes the LTL language ${\ensuremath{\mathbf{F}}} {\ensuremath{\mathbf{G}}} a \lor {\ensuremath{\mathbf{F}}} {\ensuremath{\mathbf{G}}} b$. The figure only shows the reachable states of this construction. As specified in the construction above, states of DPA are labelled with a subset of $\overline{Q_d}$ and a ordered subset of $Q_d$ of the original NBA. As an illustration of the definitions above, let us  explain the color of edges from state $(\{1\},[4,3])$ to itself on letter $b$. When the NBA is in state $1$, $3$ or $4$ and letter $b$ is read, then the next state of the automaton is again  $1$, $3$ or $4$. Note also that there are no runs that are merging in that case. As a consequence, the color that is emitted is even and equal to the index of the smallest state that is the target of an accepting transition. In this case, this is state $3$ and its index is $2$. This is the justification for the color $4$ on the edge. On the other hand, if letter $a$ is read from state  $(\{1\},[4,3])$, then the automaton moves to states $(\{1\},[4,2])$. The state $3$ is mapped to state $4$ and there is a run merging which induces that the color emitted is odd and equal to $3$. This $3$ trumps all the $4$'s that were possibly emitted from state $(\{1\},[4,3])$ before.
\end{example}

 
  \begin{theorem}
  The language defined by the deterministic parity automaton $B$ is equal to the language defined by the limit deterministic automaton $A$, i.e. $\mathsf{L}(A)=\mathsf{L}(B)$.
  \end{theorem}
  \begin{proof}
  Let $w \in \Sigma^{\omega}$ and $G_w$ be the run DAG of $A$ on $w$. It is easy to show by induction that the sequence of 
  colors that occur along $G_w$ is equal to the sequence of colors defined by the run of the automaton $B$ on $w$. By Theorem~\ref{thm:coloring}, the language of automaton $B$ is thus equal to the language of automaton $A$. \qed
  \end{proof}
  
\section{From LDBA to DPA}

\subsection{Run DAGs and their coloring}

\paragraph{{\bf Run DAG}} A nondeterministic automaton $A$ may have several (even an infinite number of) runs on a given $\omega$-word $w$. As in~\cite{DBLP:journals/tocl/KupfermanV01}, we represent this set of runs by means of a directed acyclic graph structure called the {\em run DAG} of $A$ on $w$. Given an LDBA $A=(Q,Q_d,q_0,\Sigma,\delta,\alpha)$, this graph $G_w=(V,E)$ has a set of vertices $V \subseteq Q \times {\mathbb{N}}$ and edges $E \subseteq V \times V$ defined as follows:

  \begin{itemize}
  	\item $V = \bigcup_{i \in {\mathbb{N}}} V_i$, where the sets $V_i$ are defined inductively: 
			\begin{itemize}
				\item $V_0=\{ (q_0,0) \}$, and for all $i \geq 1$, 
				\item $V_i = \{ (q,i) \mid \exists (q',i-1) \in V_{i-1} : (q',w(i),q) \in \delta \}$;
			\end{itemize}
	\item $E = \{ ((q,i),(q',i+1)) \in V_i \times V_{i+1} \mid (q,w(i),q') \in \delta \}$.
  \end{itemize} 
  \noindent
  We denote by $V^d_{i}$ the set $V_i \cap (Q_d \times \{i\})$ that contains the subset of vertices of layer $i$ that are associated with states in $Q_d$.

Observe that all the paths of $G_w$ that start from $(q_0,0)$ are runs of $A$ on $w$, and, conversely,  each run $\rho$ of $A$ on $w$ corresponds exactly to one path in $G_w$ that starts from $(q_0,0)$. So, we call {\em runs} the paths in the run DAG $G_w$. In particular, we say that an infinite path $v_0 v_1 \dots v_n \dots$ of $G_w$ is an accepting run if there are infinitely many positions $i \in {\mathbb{N}}$ such that $v_i=(q,i)$, $v_{i+1}=(q',i+1)$, and $(q,w(i),q') \in \alpha$. Clearly, $w$ is accepted by $A$ if and only if there is an accepting run in $G_w$.  We denote by $\rho(0..n)=v_0 v_1 \dots v_n$ the prefix of length $n+1$ of the run $\rho$.

\paragraph{{\bf Ordering of runs}} 
A function ${\sf Ord} : Q \rightarrow \{ 1,2,\dots,|Q_d|,+\infty\}$ is called an {\em ordering} of the states of $A$ w.r.t. $Q_d$ if  ${\sf Ord}$ defines a strict total order on the state from $Q_d$, and maps each state $q \in \overline{Q_d}$ to $+ \infty$, i.e.: 
  \begin{itemize}
	\item for all $q \in \overline{Q_d}$, ${\sf Ord}(q)=+\infty$, 
	\item for all $q \in Q_d$, ${\sf Ord}(q)\not=+\infty$, and 
	\item for all $q,q' \in Q_d$, ${\sf Ord}(q)={\sf Ord}(q')$ implies $q=q'$. 
  \end{itemize}
  \noindent
  We extend ${\sf Ord}$ to vertices in $G_w$ as follows: ${\sf Ord}((q,i))={\sf Ord}(q)$.

Starting from ${\sf Ord}$, we define the following pre-order on the set of run prefixes of the run DAG $G_w$.
Let $\rho(0..n)=v_0 v_1 \dots v_n \dots$ and $\rho'(0..n)=v'_0 v'_1 \dots v'_n \dots$ be two run prefixes of length $n+1$, we write $\rho(0..n) \sqsubseteq \rho'(0..n)$, if $\rho(0..n)$ is {\em smaller than} $\rho'(0..n)$, which is defined as:
  \begin{itemize}
  	\item for all $i$, $0 \leq i \leq n$, ${\sf Ord}(\rho(i))={\sf Ord}(\rho'(i))$, or 
	\item there exists $i$, $0 \leq i \leq n$, such that:
		\begin{itemize}
			\item ${\sf Ord}(\rho(i)) < {\sf Ord}(\rho'(i))$, and 
			\item for all $j$, $0 \leq j < i$, ${\sf Ord}(\rho(j))={\sf Ord}(\rho'(j))$. 
		\end{itemize}
  \end{itemize}
  \noindent
  This is extended to (infinite) runs as: $\rho \sqsubseteq \rho'$ iff for all $i \geq 0 \cdot {\sf Ord}(\rho(0..i)) \sqsubseteq {\sf Ord}(\rho'(0..i))$. 

\begin{remark}
If $A$ accepts a word $w$, then $A$ has a $\sqsubseteq$-smallest accepting run for $w$.
\end{remark}

We use the $\sqsubseteq$-relation on run prefixes to order the vertices of $V_i$ that belong to $Q_d$: for two different vertices $v=(q,i) \in V_i$ and $v'=(q',i) \in V_i$, $v$ is $\sqsubset_i$-smaller than $v'$, if there is a run prefix of $G_w$ that ends up in $v$ which is $\sqsubseteq$-smaller than all the run prefixes that ends up in $v'$, which induces a total order among the vertices of $V^d_i$ because the states in $Q_d$ are totally ordered by the function ${\sf Ord}$. 

\begin{lemma}
For all $i \geq 0$, for two different vertices $v=(q,i),v'=(q',i) \in V^d_i$, then either $v \sqsubset_i v'$ or $v' \sqsubset_i v$, i.e., $\sqsubset_i$ is a total order on $V^d_i$.
\end{lemma}

\paragraph{{\bf Indexing vertices}}
The index of a vertex $v=(q,i) \in V_i$ such that $q \in Q_d$, denoted by ${\sf Ind}_i(v)$, is a value in $\{1,2,\dots,|Q_d|\}$ that denotes its order in $V^d_i$ according to $\sqsubset_i$ (the $\sqsubset_i$-smallest element has index $1$). 
For $i \geq 0$, we identify two important sets of vertices:
  \begin{itemize}
  	\item ${\sf Dec}(V^d_{i})$ is the set of vertices $v \in V^d_{i}$ such that there exists a vertex $v' \in V^d_{i+1}$: $(v,v') \in E$ and ${\sf Ind}_{i+1}(v') < {\sf Ind}_{i}(v)$, i.e. the set of vertices in $V^d_{i}$ whose (unique) successor in $V^d_{i+1}$ has a smaller index value. 
	\item ${\sf Acc}(V^d_{i})$ is the set of vertices $v=(q,i) \in V^d_{i}$ such that there exists $v'=(q',i+1) \in V^d_{i+1}$: $(v,v') \in E$ and $(q,w(i),q') \in \alpha$, i.e. the set of vertices in $V^d_{i}$ that are the source of an accepting transition on $w(i)$.
  \end{itemize}

\begin{remark}
Along a run, the index of vertices can only decrease. As the function ${\sf Ind}(\cdot)$ has a finite range, the index along a run has to eventually stabilize.
\end{remark}

\paragraph{{\bf Assigning colors}}
The set of colors that are used for coloring the levels of the run DAG $G_w$ is $\{1, 2, \dots, 2\cdot|Q_d|+1\}$.
We associate a color with each transition from level $i$ to level $i+1$ according to the following set of cases:
\begin{enumerate}
	\item if ${\sf Dec}(V^d_{i})=\emptyset$ and ${\sf Acc}(V^d_i)\not=\emptyset$, the color is $2 \cdot\min_{v \in {\sf Acc}(V^d_{i})} {\sf Ind}_{i}(v)$.
	\item if ${\sf Dec}(V^d_{i})\not=\emptyset$ and ${\sf Acc}(V^d_i)=\emptyset$, the color is $2 \cdot\min_{v \in {\sf Dec}(V^d_{i})} {\sf Ind}_{i}(v)-1$.
	\item if ${\sf Dec}(V^d_{i})\not=\emptyset$ and ${\sf Acc}(V^d_i)\not=\emptyset$, the color is defined as the minimal color among 
		\begin{itemize}
			\item $c_{{\sf odd}}=2 \cdot\min_{v \in {\sf Dec}(V^d_{i})} {\sf Ind}_{i}(v)-1$, and 
			\item $c_{{\sf even}}=2 \cdot \min_{v \in {\sf Acc}(V^d_{i})} {\sf Ind}_{i}(v)$.
		\end{itemize}
	\item if ${\sf Dec}(V^d_{i})={\sf Acc}(V^d_i)=\emptyset$, the color is $2 \cdot |Q_q|+1$.
\end{enumerate}

The intuition behind this coloring is as follows: the coloring tracks runs in $Q_d$ (only those are potentially accepting as $\alpha \subseteq Q_d \times \Sigma \times Q_d$) and tries to produce an even color that corresponds to the smallest index of an accepting run. If in level $i$ the run DAG has an outgoing transition that is accepting, then this is a \textit{positive event}, as a consequence the color emitted is {\em even} and it is a function of the smallest index of a vertex associated with an accepting transition from $V_{i}$ to $V_{i+1}$. Runs in $Q_d$ are deterministic but they can merge with \textit{smaller} runs. When this happens, this is considered as a \textit{negative event} because the even colors that have been emitted by the run that merges with the smaller run should  not be taken into account anymore. As a consequence an odd color is emitted in order to cancel all the (good) even colors that were generated by the run that merges with the smaller one. In that case the odd color is function of the smallest index of a run vertex in $V_{i}$ whose run merges with a smaller vertex in $V_{i+1}$. Those two first cases are handled by cases $1$ and $2$ of the case study above. When both situations happen at the same time, then the color is determined by the minimum of the two colors assigned to the positive and the negative events. This is handled by case 3 above. And finally, when there is no accepting transition from $V_{i}$ to $V_{i+1}$ and no merging, the largest odd color is emitted as indicated by case 4 above. 

According to this intuition, we define the {\em color summary} of the run DAG $G_w$ as the minimal color that appears infinitely often along the transitions between its levels.  Because of the deterministic behavior of the automaton in $Q_d$, each run can only merge at most $| Q_d |-1$ times with a smaller one (the size of the range of the function ${\sf Ind}(\cdot)$ minus one), and as a consequence of the definition of the above coloring, we know that, on word accepted by $A$, the smallest accepting run will eventually generate infinitely many (good) even colors that are never trumped by smaller odd colors. 
\begin{figure}
	\vspace*{-1em}\myspace
 \begin{center}
        \resizebox{!}{7cm}{\input{figure2.tex}}
  \end{center}
  \vspace*{-1em}
\caption{\label{fig:run-dag} The run DAGs automaton of Fig.~\ref{fig:ex-LDBA} on the word $w=(ab)^{\omega}$ given on the left, and on the word $w=aab^{\omega}$ given on the right, together with their colorings.}
\vspace*{-1em}\myspace
\end{figure}

\begin{example}
The left part of Fig.~\ref{fig:run-dag} depicts the run DAG of the limit-deterministic automaton of Fig.~\ref{fig:ex-LDBA} on the word $w=abb(ab)^{\omega}$. Each path in this graph represents a run of the automaton on this word. The coloring of the run DAG follows the coloring rules defined above. Between level $0$ and level $1$, the color is equal to $7= 2|Q_d| + 1$, as no accepting edge is taken from level $0$ to level $1$ and no run merges (within $Q_d$). The color $7$ is also emitted from level $1$ to level $2$ for the same reason. The color $4$ is emitted from level $2$ to level $3$ because the accepting edge $(3,b,3)$ is taken and the index of state $3$ in level $2$ is equal to $2$ (state $4$ has index $1$ as it is the end point of the smallest run prefix within $Q_d$). The color $3$ is emitted from level $3$ to level $4$ because the run that goes from $3$ to $4$ merges with the smaller run that goes from $4$ to $4$. In order to cancel the even colors emitted by the run that goes from $3$ to $4$, color $3$ is emitted. It cancels the even color $4$ emitted before by this run. Afterwards, colors $3$ is emitted forever. The color summary is $3$ showing that there is no accepting run in the run DAG.

The right part of Fig.~\ref{fig:run-dag} depicts the run DAG of the limit deterministic automaton of Fig.~\ref{fig:ex-LDBA} on the word $w=aab^{\omega}$. The coloring of the run DAG follows the coloring rules defined above. Between levels $0$ and $1$, color $7$ is emitted because no accepting edge is crossed. To the next level, we see the accepting edge $(2,a,2)$ and color $2\cdot1=2$ is emitted.
Upon reading the first $b$, we see again $7$ since there is neither any accepting edge seen nor any merging takes place. 
Afterwards, each $b$ causes an accepting edge $(3,b,3)$ to be taken. While the smallest run, which visits $4$ forever, is not accepting, the second smallest run that visits $3$ forever is accepting. As $3$ has index $2$ in all the levels below level $3$, the color is forever equal to $4$. The color summary of the run is thus equal to $2\cdot 2=4$ and this shows that word $w=aab^{\omega}$ is accepted by our limit deterministic automaton of Fig.~\ref{fig:ex-LDBA}.
\end{example}

The following theorem tells us that the color summary (the minimal color that appears infinitely often) can be used to identify run DAGs that contain accepting runs. The proof can be found in Appendix~\ref{app:coloring}.

\begin{theorem} \label{thm:coloring}
The color summary of the run DAG $G_w$ is even if and only if there is an accepting run in $G_w$.
\end{theorem}

\section{From LTL to Parity in $2^{2^{\mathcal O(n)}}$}

In \cite{DBLP:conf/cav/SickertEJK16} we present a LTL$\rightarrow$LDBA translation. Given a formula 
$\varphi$ of size $n$, the translation produces an asymptotically optimal LDBA with $2^{2^{\mathcal O(n)}}$ states. 
The straightforward composition of this translation with the single exponential 
LDBA$\rightarrow$DPA translation of the previous section is only guaranteed to be 
triple exponential, while the Safra-Piterman construction produces a DPA of at most doubly 
exponential size. In this section we describe a modified composition that yields a double 
exponential DPA.
To the best of our knowledge this is is the first translation of the whole LTL to deterministic parity automata that is asymptotically optimal and does not use Safra's construction.

The section is divided into two parts. 
In the first part, we explain and illustrate a redundancy occurring in our LDBA$\rightarrow$DPA translation, responsible for the undesired extra exponential.
We also describe an optimization that removes this redundancy when the LDBA satisfies some conditions.
In the second part, we show these conditions are satisfied on the products of the LTL$\rightarrow$LDBA translation, which in turn guarantees a doubly exponential LTL$\rightarrow$DPA procedure. 

\subsection{An improved construction}

We can view the second component of a state of the DPA as a sequence of states of the LDBA, ordered by their indices.
Since there are $2^{2^{\mathcal O(n)}}$ states of the LDBA for an LTL formula of length $n$, the number of such sequences is 
$$2^{2^{\mathcal O(n)}}!=2^{2^{2^{\mathcal O(n)}}}$$
If only the length of the sequences (the maximum index) were bounded by $2^n$, the number of such sequences would be smaller than the number of functions $2^n\to 2^{2^{\mathcal O(n)}}$ which is
$$(2^{2^{\mathcal O(n)}})^{2^n}=2^{2^{\mathcal O(n)}\cdot 2^n}=2^{2^{\mathcal O(n)}}$$

Fix an LDBA with set of states $Q$. Assume the existence of an {\em oracle}: a list of statements of the form $\mathsf{L}(q) \subseteq \bigcup_{q' \in Q_q} \mathsf{L}(q')$ where $q \in Q$ and $Q_q \subseteq Q$.  We use the oracle to define a mapping that associates to each run DAG $G_w$ a ``reduced DAG'' $G_w^*$, defined as the result of iteratively performing the following four-step operation:
\begin{itemize}
\item Find the first $V_i$ in the current DAG such that the sequence $(v_1,i)\sqsubset(v_2,i)\sqsubset\cdots\sqsubset(v_{n_i},i)$ of vertices of 
$V_i^d$ contains a vertex $(v_k,i)$ for which the oracle ensures
\begin{equation}
\mathsf{L}(v_k)\subseteq\bigcup_{j<k}\mathsf{L}(v_j) \tag{$*$}\label{eq:lang-based}
\end{equation}
\noindent We call $(v_k, i)$ a {\em redundant vertex}.
\item Remove $(v_k, i)$ from the sequence, and otherwise keep the ordering $\sqsubseteq_i$ unchanged (thus decreasing the index of vertices $(v,\ell)$ with $\ell>k$). 
\item Redirect transitions leading  from vertices in $V_{i-1}$ to $(v_k, i)$ so that they lead to the smallest vertex $(v_1, i)$ of $V_i$. 
\item Remove any vertices (if any) that are no longer reachable from vertices of $V_1$. 
\end{itemize}
We define the color summary of $G_w^*$ in exactly the same way as the color summary of $G_w$.
The DAG $G_w^*$ satisfies the following crucial property, whose proof can be found in Appendix~\ref{app:merging}:
\begin{proposition}\label{prop:merging}
	The color summary of the run DAG $G_w^*$ is even if and only if there is an accepting run in $G_w$.
\end{proposition}

The mapping on DAGs induces a reduced DPA as follows. The states are the 
pairs $(s, (t, <))$ such that $(t, <)$ does not contain redundant vertices.
There is a transition $(s_1, (t_1, <)) \stackrel{a}{\rightarrow} 
(s_2, (t_2, <))$ with color $c$ if{}f there is a word $w$ and an index $i$ such that  $(s_1, (t_1, <))$ and $(s_2, (t_2, <))$ correspond to the $i$-th and $(i+1)$-th levels of $G_w^*$, and $a$ and $c$ are the letter and color of the step between these levels in $G_w^*$. Observe that the set of transitions is independent of the words chosen to define them.

The equivalence between the initial DPA $\mathcal A$ and the reduced DPA $\mathcal A_r$ follows immediately from Proposition \ref{prop:merging}: $\mathcal A$ accepts $w$ if{}f $G_w$ contains an accepting run if{}f the color summary of $G_w^*$ is even if{}f $\mathcal A_r$ accepts $w$.

\begin{example}
	Consider the LDBA of Fig.~\ref{fig:ex-LDBA} and an oracle given by $\mathsf{L}(4)=\emptyset$, ensuring $\mathsf{L}(4)\subseteq\bigcup_{i\in I}\mathsf{L}(i)$ for any $I\subseteq Q$. Then $4$ is always redundant and merged, removing the two rightmost states of the DPA of Fig.~\ref{fig:DPA-ex} (left), resulting in the DPA of Fig.~\ref{fig:DPA-ex} (right). 
	However, for the sake of technical convenience, we shall refrain from removing a redundant vertex when it is the smallest one (with index $1$).
\end{example}

Since the construction of the reduced DPA is parametrized by an oracle,
the obvious question is how to obtain an oracle that does not involve applying an expensive language inclusion test. Let us give a first example in which an oracle can be easily obtained: 

\begin{example}
	Consider an LDBA where each state $v=\{s_1,\ldots,s_k\}$ arose from some powerset construction on an NBA in such a way that $\mathsf{L}(\{s_1,\ldots,s_k\})=\mathsf{L}(s_1)\cup\cdots\mathsf{L}(s_k)$. An oracle can, for instance, allow us to merge whenever $v_k\subseteq\bigcup_{j<k}v_j$, which is a sound syntactic approximation of language inclusion. 
	This motivates the following formal generalization.
\end{example}

Let $\mathcal L_B=\{L_i\mid i\in B\}$ be a finite set of languages, called \emph{base} languages.
We call $\mathcal L_C:=\{\bigcup\mathcal L\mid\mathcal L\subseteq\mathcal L_B\}$ the join-semilattice of \emph{composed} languages.
We shall assume an LDBA with some $\mathcal L_B$ such that $\mathsf{L}(q)\in\mathcal L_C$ for every state $q$.
We say that such an LDBA \emph{has a base} $\mathcal L_B$.
In other words, every state recognizes a union of some base languages.
(Note that every automaton has a base of at most linear size.)
Whenever we have states $v_j$ recognizing $\bigcup_{i\in I_j}L_i$ with $I_j\subseteq B$ for every $j$, the oracle allows us to merge vertices $v_k$ satisfying $I_k\subseteq \bigcup_{j<k}I_j$.
Intuitively, the oracle declares a vertex redundant  whenever the simple syntactic check on the indices allows for that.

Let $V_1=\bigcup_{i\in I_1}L_i,\cdots V_j=\bigcup_{i\in I_j}L_i$ be a sequence of languages of $\mathcal L_C$ where the reduction has been applied and there are no more redundant vertices. The maximum length of such a sequence
is given already by the base $\mathcal L_B$ and we denote it $\mathit{width}(\mathcal L_B)$.
\begin{lemma}
	For any $\mathcal L_B$, we have $\mathit{width}(\mathcal L_B)\leq|\mathcal L_B|+1$.
\end{lemma}
\begin{proof}
	We provide an injective mapping of languages in the sequence (except for $V_1$) into $B$.	
	Since $I_2\not\subseteq I_1$, there is some $i\in I_2\setminus I_1$ and we map $V_2$ to this $i$.
	In general, since $I_k\not\subseteq \bigcup_{j=1}^{k-1}I_j$, we also have $i\in I_k\setminus \bigcup_{j=1}^{k-1}I_j$ and we map $V_k$ to this $i$.\qed
\end{proof}


On the one hand, the transformation of LDBA to DPA without the reduction yields $2^{\mathcal O(|Q|\cdot\log|Q|)}$ states.
On the other hand, we can now show that the second component of reduced LDBA with a base can be exponentially smaller. Further, let us assume the LDBA is \emph{initial-deterministic}, meaning that $\delta\cap(\overline{Q_d}\times\Sigma\times\overline{Q_d})$ is deterministic, thus not resulting in blowup in the first component.

\begin{corollary}\label{cor:base}
	For every initial-deterministic LDBA with base of size $m$, there is an equivalent DPA with $2^{\mathcal O(m^2)}$ states.
\end{corollary}
\begin{proof}
	The number of composed languages is $\mathcal L_C=2^{m}$.
	Therefore, the LDBA has at most $2^m$ (non-equivalent) states.
	Hence the construction produces at most
	$$|\mathcal L_C|\cdot|\mathcal L_C|^{\mathcal O(\mathit{width}(\mathcal L_B))}=2^m\cdot(2^m)^{\mathcal O(m)}=2^{\mathcal O(m^2)}$$
	states since the LDBA is initial-deterministic, causing no blowup in the first component. \qed
\end{proof}

\subsection{Bases for LDBAs Obtained from LTL Formulas}

We prove that the width for LDBA arising from the LTL transformation is only singly exponential in the formula size.
To this end, we need to recall a property of the LTL$\rightarrow$LDBA translation of \cite{DBLP:conf/cav/SickertEJK16}.
Since partial evaluation of formulas plays a major role in the translation, we introduce the following definition.
Given an LTL formula $\varphi$ and sets $T$ and $F$ of LTL formulas, let $\varphi[T,F]$ denote the result of substituting ${\ensuremath{\mathbf{tt}}}$ (true) for each occurrence of a formula of $T$ in $\varphi$, and similarly ${\ensuremath{\mathbf{ff}}}$ (false) for formulas of $F$.
The following property of the translation is proven in Appendix~\ref{app:ltl}.

\begin{proposition}\label{prop:translation}
	For every LTL formula $\varphi$, every state $s$ of the LDBA of \cite{DBLP:conf/cav/SickertEJK16} is labelled by an LTL formula $\mathit{label}(s)$ such that (i) $\mathsf{L}(s)=\mathsf{L}(\mathit{label}(s))$ and (ii) $\mathit{label}(s)$ is a Boolean combination of subformulas of $\varphi[T_s, F_s]$ for some $T_s$ and $F_s$.
	Moreover, the LDBA is initial-deterministic.
\end{proposition}

 As a consequence, we can bound the corresponding base:

\begin{corollary}\label{cor:ltl}
	For every LTL formula $\varphi$, the LDBA of \cite{DBLP:conf/cav/SickertEJK16} for $\varphi$ has a base of size $2^{\mathcal O{(|\varphi|)}}$.
\end{corollary}
\begin{proof}
Firstly, we focus on states using the same $\varphi[T_s, F_s]$.
The language of each state can be defined by a Boolean formula over $\mathcal O (|\varphi|)$ atoms.
Since every Boolean formula can be expressed in the disjunctive normal form, its language is a union of the conjuncts.
The conjunctions thus form a base for these states.
There are exponentially many different conjunction in the number of atoms.
Hence the base is of singly exponential size $2^{\mathcal O(|\varphi|)}$ as well.

Secondly, observe that there are only $2^{\mathcal O(|\varphi|)}$ different formulas $\varphi[T_s, F_s]$ and thus only $2^{\mathcal O(|\varphi|)}$ different sets of atoms.	
Altogether, the size is bounded by 
\begin{equation*}
2^{\mathcal O(|\varphi|)}\cdot 2^{\mathcal O (|\varphi|)}= 2^{\mathcal O (|\varphi|)} \tag*{$\square$}
\end{equation*}
\end{proof}

\begin{theorem}
	For every LTL formula $\varphi$, there is a DPA with $2^{2^{\mathcal O(|\varphi|)}}$ states.
\end{theorem}
\begin{proof}
The LDBA for $\varphi$ has base of singly exponential size $2^{\mathcal O(|\varphi|)}$ by Corollary~\ref{cor:ltl} and is initial-deterministic by Proposition~\ref{prop:translation}. Therefore, by Corollary \ref{cor:base}, the size of the DPA is doubly exponential, in fact
\begin{equation*}
2^{{(2^{\mathcal O(|\varphi|)})}^2}=2^{2^{\mathcal O(|\varphi|)}} \tag*{$\square$}
\end{equation*}
\end{proof}
This matches the lower bound $2^{2^{\Omega(n)}}$ by \cite{DBLP:conf/mochart/KupfermanR10} as well as the upper bound by the Safra-Piterman approach. Finally, note that while the breakpoint constructions in \cite{DBLP:conf/cav/SickertEJK16} is analogous to Safra's vertical merging, the merging introduced here is analogous to Safra's horizontal merging.

\section{Optimisations}

\subsection{Parallelisation}

Since multiple cores are abundant these days, we use a simple trick to obtain small automata: we launch two threads for $\varphi$ and $\neg \varphi$ and compute the DPA. Observe that complementing parity automata is cheap, since we just need to change the parity of the acceptance condition. We then return the smaller automaton and also prematurely cancel one of the translations, if we already know that the running translation will produce a larger automaton.

\subsection{Reduction of Rankings}

Since we can freely change the order of states we jump to, a good heuristic is to sort jumps to accepting components that are labelled with ${\ensuremath{\mathbf{F}}}$-Operators---more precisely, belong to the syntactic class of pure eventual formulas---before any other accepting component. The reasoning is that components for the pure eventual fragment will never be removed from the ranking. Analogously, if an accepting component is only labeled with formulas from the $({\ensuremath{\mathbf{X}}}, a)$-fragment, a safety language is described. These are volatile in the sense that after a fixed number of steps---the nesting depth of the ${\ensuremath{\mathbf{X}}}$'s---we know if the obligations are fulfilled or not. Thus we do not need to track all these components. Just one at a time and whenever one of these fails we switch to the next one.

\section{Preliminaries}

\myspacet
\section{Proof of Theorem \ref{thm:coloring}}\label{app:coloring}

\begin{reftheorem}{thm:coloring}
The color summary of the run DAG $G_w$ is even if and only if there is an accepting run in $G_w$.
\end{reftheorem}

\begin{proof}
	``$\Rightarrow$'':
Assume that the color summary of $G_w$ is even and equal to $c$. Then it must be the case that there exists a level $i \geq 0$ such the color after level $i$ is always larger than or equal to $c$, and infinitely many times equal to $c$. W.l.o.g. assume that in level $i$, there exists a vertex $v=(q,i) \in {\sf Acc}(V^d_i)$ and $c=2 \cdot {\sf Ind}(v)$. Take the smallest run prefix that ends up in $v$, this run prefix will never merge with a smaller run prefix and all smaller run prefixes that are active in level $i$ will not merge, as otherwise, there would exist a position $j \geq i$ where the index of the run that passes by $(q,i)$ would decrease and this would contradict the fact that for all $j \geq i$, all the colors that are emitted are larger than or equal to $c$. Let us now consider the suffix of the run that pass by $v=(q,i)$. As the even color $c$ is emitted infinitely many times after level $i$, we know that this run suffix crosses infinitely many times $\alpha$. So this run is accepting and this is the smallest such run. 

``$\Leftarrow$'':

(Step 1):
Now, let us consider the other direction. Assume that there exists an accepting run of $A$ on a word $w$. We first establish the existence of a run $\rho$ which is accepting and for which there exists a position $k \geq 0$ from which $\rho$ does not merge with any smaller run, and all smaller runs are non accepting. We identify $\rho$ and $k$ as follows. Among the accepting runs, we select one that enters first in the set of states $Q_d$ say at level $i \geq 0$. They can be several of them but we take one that enters $Q_d$ via a state $q$ of minimal index for ${\sf Ord}$. Let $V_i^d$ be the active states at level $i$ that are in $Q_d$. The way we have chosen $q$ make sure that all the states in $V^d_i$ with a smaller index than $q$ are the origin of non accepting runs and clearly as $\rho$ is accepting it cannot merge with one of those smaller runs. Now, some of those smaller runs may merge in the future, and each time they merge, the index of $\rho$ will decrease. But this will happen a number of times which is bounded by $Q_d$. 

(Step 2): 
Let $k$ be the position when the last merge of a smaller run pefix happens.

(Step 3): 
Let us now show that the existence of $\rho$ and this position $k$ allow us to prove that the color summary is even. After position $k$, there are only odd colors with values larger than or equal to $2 \cdot {\sf Ind}(\rho(k))+1$ because we know that nor $\rho$ neither smaller runs merge in the future. Also as $\rho$ is accepting, there will be an infinite number of positions $l \geq k$ where the even color is equal to $2 \cdot {\sf Ind}(\rho(k)))$, and only finitely many positions after $k$ may have an even color which is less than this value as all runs that are smaller than $\rho$ are not accepting. So the summary color is even and equal to $2 \cdot {\sf Ind}(\rho(k)))$.
\end{proof}