As for the many disjunctions and conjunctions that appear in the formulas,
observe that the number of disjuncts and conjuncts does not depend on the
formula-parameters $\beta$ and $\tau$, but only the level $i$ of the
configurations $S$, $B$, and $T$. Hence, they do not dominate the growth rate
of the overall formula length.

lemmaReachFormulaSize Consider a reset cascade ${\cal A}$ with $n$ levels and
up to $n$ states in each level, and a formula
$\zeta=S\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.71559pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.71559pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.71559pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{B(\beta)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.71559pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.71559pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.71559pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{B(\beta)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.71559pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.71559pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.71559pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{B(\beta)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.71559pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.71559pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.71559pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{B(\beta)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa 04B}\\!\\!\scriptscriptstyle{}}}T\left(\tau\right)$ with
configurations $S$, $B$ and $T$ of ${\cal A}$ of level $i\leq n$. Let
$d=\max(0pt{\beta},0pt{\tau})$ and let $l=\max(|\beta|,|\tau|)$. Then:

$(a)\leavevmode\nobreak\ 0pt{\zeta}\leq d+3^{i}\quad\text{ and
}\quad(b)\leavevmode\nobreak\ |\zeta|\leq l\cdot(10|\Sigma|^{2}n)^{4^{i}}$

Section 4.3 is proven by induction on $i$. The details are given in Section
0.A.4.

###  4.4 Translating Deterministic Counter-Free Automata to LTL

We use the reachability formulas of Section 4.2 to translate a reset cascade
${\cal A}$ to an equivalent LTL formula. Our LTL formulation of ${\cal A}$’s
acceptance condition is based on an LTL formulation of “$C$ is visited
finitely/infinitely often along a run of ${\cal A}$ on a word $w$”, for a
given configuration $C$ of ${\cal A}$. It thus applies to every
$\omega$-regular acceptance condition and by Sections 4.1 and 3 to every
deterministic counter-free $\omega$-regular automaton. We introduce two
shorthands to the main reachability formula: the first is satisfied if we
reach $T$ from $S$ without any side constraints (which is always satisfied in
the case that $S=T$), and the second requires that we reach it along a
nonempty prefix.

$S\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa 04B}\\!\\!\scriptscriptstyle{}}}T\coloneqq
S\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{T({\mathbf{false}})}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{T({\mathbf{false}})}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{T({\mathbf{false}})}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{T({\mathbf{false}})}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptscriptstyle{}}}T\left({\mathbf{true}}\right)\quad\quad
S\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
$}}^{\hbox{\set@color$\scriptstyle\,>0$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
$}}^{\hbox{\set@color$\scriptstyle\,>0$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
$}}^{\hbox{\set@color$\scriptstyle\,>0$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
$}}^{\hbox{\set@color$\scriptstyle\,>0$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\scriptscriptstyle{}}}T\coloneqq\bigvee_{\sigma\in\Sigma}\left(\sigma\land{\mathbf{X}}(\delta(S,\sigma)\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa 04B}\\!\\!\scriptscriptstyle{}}}T)\right)$

With Sections 4.2 and 4.2 we then obtain (a proof is given in Section 0.A.5):

lemmaLTLforVisitFinitelyOften Consider a reset cascade ${\cal A}=\langle
2^{AP},{\cal A}_{1},\dots,{\cal A}_{n}\rangle$ together with an initial
configuration $\iota$ and some configuration $C$. Then for a word
$w\in{(2^{AP})}^{\omega}$, the run of ${\cal A}$ on $w$ starting in $\iota$
visits $C$ finitely often iff $w$ satisfies the formula
${\mathit{Fin}}(C)\coloneqq\neg(\text{\Large$\iota$}\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptscriptstyle{}}}C)\lor\text{\Large$\iota$}\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptscriptstyle{}}}C(\neg(C\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
$}}^{\hbox{\set@color$\scriptstyle\,>0$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
$}}^{\hbox{\set@color$\scriptstyle\,>0$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
$}}^{\hbox{\set@color$\scriptstyle\,>0$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
$}}^{\hbox{\set@color$\scriptstyle\,>0$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\scriptscriptstyle{}}}C))$. Furthermore,
${\mathit{Fin}}(C)\in\Sigma_{2}$.

We are now in position to give our main result.

theoremAutomatonToLTL Every counter-free deterministic $\omega$-regular
automaton ${\cal D}$ over alphabet $2^{AP}$ with $n$ states (and any
acceptance condition) is equivalent to an LTL formula $\varphi$ over atomic
propositions $AP$ of double-exponential temporal-nesting depth $($in
$O(2^{2^{n}}))$ and triple-exponential length $($in $2^{2^{O(2^{n})}})$. If
${\cal D}$ is a looping-Büchi, looping-coBüchi, weak, Büchi, coBüchi, or
Muller automaton then $\varphi$ is respectively in the
$\Pi_{1},\Sigma_{1},\Delta_{1},\Pi_{2},\Sigma_{2}$, or $\Delta_{2}$ syntactic
fragment of LTL.

###### Proof.

We first prove the general result, w.r.t. an arbitrary counter-free
deterministic automaton ${\cal D}$, and then take into account ${\cal D}$’s
acceptance condition, to establish the last part of the theorem.

Consider a counter-free deterministic $\omega$-regular automaton ${\cal D}$
with some acceptance condition and $n$ states. Recall that there is a Muller
automaton ${\cal D}^{\prime}$ equivalent to ${\cal D}$ over the semiautomaton
of ${\cal D}$. By Propositions 3 and 4.1, ${\cal D}^{\prime}$ is equivalent to
a deterministic Muller automaton ${\cal D}^{\prime\prime}$ that is described
by a reset cascade ${\cal A}$ with up to $m=2^{n}$ levels and $m$ states in
each level (and thus up to $m^{m}$ configurations), and whose acceptance
condition has up to $k\in 2^{O(m^{m}n)}=2^{O(m^{m})}$ acceptance sets. An LTL
formula $\varphi$ equivalent to ${\cal D}$ can be defined by formulating the
acceptance condition of ${\cal D}^{\prime}$ along Section 4.4.

Recall that the Muller condition is a $k$-elements disjunction, where each
disjunct $M$ is a conjunction of requirements to visit infinitely often every
configuration from some set $G$ and finitely often every configuration not in
$G$. Observe that $M$ can be formulated as a disjunction over all the
configurations in ${\cal D}^{\prime\prime}$ (at most $m^{m}$), having for each
configuration $C$ the LTL formula ${\mathit{Fin}}(C)$ or
$\neg{\mathit{Fin}}(C)$, as defined in Section 4.4, depending on whether or
not $C\in G$. Hence, the overall formula $\varphi$ is a combination of
disjunctions and conjunctions of up to $k\cdot m^{m}$ subformulas of the form
${\mathit{Fin}}(C)$ or $\neg{\mathit{Fin}}(C)$. Therefore, the depth of
$\varphi$ is the same as of ${\mathit{Fin}}(C)$, while $|\varphi|\in
O(km^{m}|{\mathit{Fin}}(C)|)\leq 2^{O(m^{m})}|{\mathit{Fin}}(C)|$. For
calculating $0pt{{\mathit{Fin}}(C)}$ and $|{\mathit{Fin}}(C)|$, we use Section
4.3 bottom up over the subformulas of ${\mathit{Fin}}(C)$.

##### Depth.

$0pt{\text{\Large$\iota$}\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa 04B}\\!\\!\scriptscriptstyle{}}}C}\leq
3^{m}\leavevmode\nobreak\ ;\leavevmode\nobreak\
0pt{C\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
$}}^{\hbox{\set@color$\scriptstyle\,>0$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
$}}^{\hbox{\set@color$\scriptstyle\,>0$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
$}}^{\hbox{\set@color$\scriptstyle\,>0$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
$}}^{\hbox{\set@color$\scriptstyle\,>0$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\scriptscriptstyle{}}}C}\leq 3^{m}+1$

$0pt{\text{\Large$\iota$}\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptscriptstyle{}}}C(\neg(C\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
$}}^{\hbox{\set@color$\scriptstyle\,>0$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
$}}^{\hbox{\set@color$\scriptstyle\,>0$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
$}}^{\hbox{\set@color$\scriptstyle\,>0$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
$}}^{\hbox{\set@color$\scriptstyle\,>0$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\scriptscriptstyle{}}}C))}\leq 2\cdot 3^{m}+1$

$0pt{{\mathit{Fin}}(C)}=\max(3^{m},2\cdot 3^{m}+1)\in O(3^{m})=O(2^{2^{n}})$,

implying $0pt{\varphi}\in O(2^{2^{n}})$.

##### Length.

$|\text{\Large$\iota$}\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptscriptstyle{}}}C|\leq(10|\Sigma|^{2}m)^{4^{m}}\leavevmode\nobreak\
;\leavevmode\nobreak\
|C\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
$}}^{\hbox{\set@color$\scriptstyle\,>0$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
$}}^{\hbox{\set@color$\scriptstyle\,>0$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
$}}^{\hbox{\set@color$\scriptstyle\,>0$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
$}}^{\hbox{\set@color$\scriptstyle\,>0$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\scriptscriptstyle{}}}C|\leq(4|\Sigma|)\cdot(10|\Sigma|^{2}m)^{4^{m}}$

$|\text{\Large$\iota$}\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\ $}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptscriptstyle{}}}C(\neg(C\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
$}}^{\hbox{\set@color$\scriptstyle\,>0$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
$}}^{\hbox{\set@color$\scriptstyle\,>0$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
$}}^{\hbox{\set@color$\scriptstyle\,>0$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\leavevmode\nobreak\
\leavevmode\nobreak\ \leavevmode\nobreak\
$}}^{\hbox{\set@color$\scriptstyle\,>0$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\scriptscriptstyle{}}}C))|\leq(4|\Sigma|(10|\Sigma|^{2}m)^{4^{m}}+1)(10|\Sigma|^{2}m)^{4^{m}}\in(|\Sigma|m)^{2^{O(m)}}$

$|{\mathit{Fin}}(C)|\in
2+(10|\Sigma|^{2}m)^{4^{m}}+(|\Sigma|m)^{2^{O(m)}}\in(|\Sigma|m)^{2^{O(m)}}$.

Therefore, $|\varphi|\in
2^{O(m^{m})}\cdot(m^{m})\cdot((|\Sigma|m)^{2^{O(m)}})=|\Sigma|^{2^{O(m)}}$.

Expressing the length of $\varphi$ with respect to the number $n$ of states in
the automaton ${\cal D}$, and taking into account the fact that the alphabet
$\Sigma$ has at most $n^{n}$ different letters (any additional letter must
have the same behavior as another letter), we have:
$|\varphi|\in|\Sigma|^{2^{O(2^{n})}}\leq(2^{n})^{2^{O(2^{n})}}=2^{2^{O(2^{n})}}$.

We now sketch the second part of the theorem connecting the syntactic
hierarchy and the different acceptance conditions of ${\cal D}$. We only
consider the cases in which ${\cal D}$ is either a Muller or a coBüchi
automaton. The complete analysis is given in Section 0.A.5. If ${\cal D}$ is a
Muller automaton, then the overall formula $\varphi$ is in $\Delta_{2}$, since
it is a Boolean combination of ${\mathit{Fin}}(C)$ formulas, which by Section
4.4 belong to $\Sigma_{2}$. If ${\cal D}$ is a coBüchi automaton, then we
construct the formula $\varphi$ directly from the coBüchi condition $\alpha$:
$\varphi$ is a conjunction of ${\mathit{Fin}}(C)$ formulas over all
configurations $C$ that are mapped to states in $\alpha$. As
${\mathit{Fin}}(C)$ belongs to $\Sigma_{2}$, so does $\varphi$. ∎

Observe that by Section 4.4, we get the following result, extending the result
of [39, Theorem 3.2] that only considers Rabin automata.

######  Corollary 1.

Every counter-free deterministic $\omega$-regular automaton (with any
acceptance condition) recognises an LTL-definable language.

###### Proof.

Recall that every deterministic $\omega$-regular automaton is equivalent to a
deterministic Muller automaton over the same semiautomaton (see, e.g., [3]).
The claim is then a direct consequence of Section 4.4. ∎

######  Remark 2.

Section 4.4 can be adapted to the finite-word setting. While on infinite
words, the ne${\mathbf{X}}$t operator is self-dual, i.e.,
$\neg{\mathbf{X}}\psi$ is equivalent to ${\mathbf{X}}\neg\psi$, over finite
words, this equivalence does not hold on words of length 1. Thus
${\mathbf{X}}$ gains a dual _weak next_ , defined as
$\tilde{{\mathbf{X}}}\psi\coloneqq\neg{\mathbf{X}}\neg\psi$. In the finite
word case, syntactic cosafety (safety) formulas are constructed from
${\mathbf{true}}$, ${\mathbf{false}}$, $a$, $\neg a$, $\vee$, $\wedge$, and
the temporal operators ${\mathbf{U}}$ and ${\mathbf{X}}$ (${\mathbf{R}}$ and
$\tilde{{\mathbf{X}}}$). Observe that ${\mathbf{X}}$ and
$\tilde{{\mathbf{X}}}$ differ only on words of length 1, and thus the only
required change in our translation scheme is to replace some ${\mathbf{X}}$s
with $\tilde{{\mathbf{X}}}$s in the reachability formula 4. For finite words a
translation of a counter-free DFA to an LTL formula with only a double
exponential size blow-up is known [42]; however, unlike our translation, it
does not guarantee syntactic safety (cosafety) formulas for safety (cosafety)
languages.

Lastly, we provide a corollary on looping automata, using Section 4.4 and the
following known result.

######  Proposition 4 (Rephrased Theorem 13 from [29]).

Let ${\cal D}$ be a deterministic looping-Büchi automaton with $n$ states that
recognises an LTL-definable language. Then there exists an equivalent counter-
free deterministic looping-Büchi automaton ${\cal D}^{\prime}$ with at most
$n$ states.

######  Corollary 2.

Every deterministic looping-Büchi (looping-coBüchi) automaton with $n$ states
that recognises an LTL-definable language is equivalent to an LTL formula
$\varphi\in\Pi_{1}$ ($\Sigma_{1}$) of temporal nesting depth in $O(2^{2^{n}})$
and length in $2^{2^{O(2^{n})}}.$

This is an elementary upper bound for two constructions for which either the
upper bound was unknown or non-elementary: the liveness-safety decomposition
of LTL [29] and the translation of semantic safety LTL to syntactic safety
LTL.

##  5 Conclusions

We have studied the size trade-offs between LTL and automata. Over a unary
alphabet, the situation is straightforward and we provided tight complexity
bounds. The general case of infinite words over an arbitrary alphabet is more
complex. We gave to our knowledge the first elementary complexity bound on the
translation of counter-free deterministic $\omega$-regular automata into LTL
formulas.

Every $\omega$-regular automaton recognising an LTL-definable language can be
translated to a counter-free deterministic automaton [39, Theorem 3.2]. Yet,
we are unaware of a bound on the size blow-up involved in such a translation.
Once established, it can be combined with our translation to get a general
bound on the translation of automata to LTL. It will also provide a (currently
unknown333In consultation with the author of [30], we have confirmed that
while the lower bound provided in that paper holds, the stated upper bound is
erroneous.) elementary upper bound on the translation of LTL with both future
and past operators to LTL with only future operators (which is the version of
LTL that we have considered), as (both version of) LTL can be translated to
nondeterministic Büchi automata with a single exponential size blow-up [41,
Theorem 2.1].

While going from non-elementary to double-exponential depth and triple-
exponential length is an improvement, these upper bounds might not be
tight—there is currently no known non-linear lower bound! Closing this gap is
a challenging open problem, which might require new lower bound techniques for
alternating automata, as LTL formulas are an inherently alternating model.

##### Acknowledgements.

We thank Moshe Vardi and Orna Kupferman for suggesting studying the
succinctness gap between semantic and syntactic safe formulas, and Mikołaj
Bojańczyk for answering our questions on algebraic automata theory.

## References

  * [1] Birget, J.C.: Two-way automata and length-preserving homomorphisms. Mathematical Systems Theory 29(3), 191–226 (1996)
  * [2] Bojańczyk, M.: Languages recognised by finite semigroups, and their generalisations to objects such as trees and graphs, with an emphasis on definability in monadic second-order logic (2020)
  * [3] Boker, U.: Why these automata types? In: Proc. of LPAR. pp. 143–163 (2018)
  * [4] Boker, U., Kupferman, O.: The quest for a tight translation of Büchi to co-Büchi automata. In: Fields of Logic and Computation, pp. 147–164. Springer (2010)
  * [5] Boker, U., Lehtinen, K., Sickert, S.: On the translation of automata to linear temporal logic. In: Bouyer, P., Schröder, L. (eds.) FOSSACS 2022. Lecture Notes in Computer Science, vol. 13242, pp. 140–160. Springer (2022). https://doi.org/10.1007/978-3-030-99253-8_8
  * [6] Cerná, I., Pelánek, R.: Relating hierarchy of temporal properties to model checking. In: MFCS. Lecture Notes in Computer Science, vol. 2747, pp. 318–327. Springer (2003)
  * [7] Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. J. ACM 28(1), 114–133 (Jan 1981)
  * [8] Chang, E.Y., Manna, Z., Pnueli, A.: Characterization of temporal property classes. In: Kuich, W. (ed.) Automata, Languages and Programming, 19th International Colloquium, ICALP92, Vienna, Austria, July 13-17, 1992, Proceedings. Lecture Notes in Computer Science, vol. 623, pp. 474–486. Springer (1992)
  * [9] Chrobak, M.: Finite automata and unary languages. Theoretical Computer Science 47, 149–158 (1986)
  * [10] Cohen, J., Perrin, D., Pin, J.E.: On the expressive power of temporal logic. Journal of computer and System Sciences 46(3), 271–294 (1993)
  * [11] Cohen-Chesnot, J.: On the expressive power of temporal logic for infinite words. Theoretical Computer Science 83(2), 301–312 (1991)
  * [12] Colcombet, T., Zdanowski, K.: A tight lower bound for determinization of transition labeled Büchi automata. In: International Colloquium on Automata, Languages, and Programming. pp. 151–162. Springer (2009)
  * [13] Diekert, V., Gastin, P.: First-order definable languages. In: Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas]. Texts in Logic and Games, vol. 2, pp. 261–306 (2008)
  * [14] Eilenberg, S.: Automata, Languages, and Machines Volume B. Academic Press, Inc., USA (1976)
  * [15] Etessami, K., Vardi, M.Y., Wilke, T.: First-order logic with two variables and unary temporal logic. Inf. Comput. 179(2), 279–295 (2002)
  * [16] Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Proc. of POPL. p. 163–173. New York, NY, USA (1980)
  * [17] Geffert, V., Mereghetti, C., Pighizzini, G.: Complementing two-way finite automata. Information and Computation 205(8), 1173–1187 (2007)
  * [18] Kamp, J.A.W.: Tense logic and the theory of linear order. University of California, Los Angeles (1968)
  * [19] Kupferman, O., Rosenberg, A.: The blowup in translating LTL to deterministic automata. In: Proc. of Model Checking and Artificial Intelligence. pp. 85–94 (2010)
  * [20] Kupferman, O., Ta-Shma, A., Vardi, M.Y.: Counting with automata. In: Proc. of LICS (1999)
  * [21] Kupferman, O., Vardi, M.Y.: Weak alternating automata are not that weak. ACM Transactions on Computational Logic (TOCL) 2(3), 408–429 (2001)
  * [22] Ladner, R.E.: Application of model theoretic games to discrete linear orders and finite automata. Information and Control 33(4), 281–303 (1977)
  * [23] Leiss, E.: Succinct representation of regular languages by boolean automata. Theoretical computer science 13(3), 323–330 (1981)
  * [24] Löding, C.: Optimal bounds for transformations of $\omega$-automata. In: Rangan, C.P., Raman, V., Ramanujam, R. (eds.) Foundations of Software Technology and Theoretical Computer Science. pp. 97–109. Springer Berlin Heidelberg, Berlin, Heidelberg (1999)
  * [25] Maler, O.: On the Krohn-Rhodes cascaded decomposition theorem. In: Time for Verification, Essays in Memory of Amir Pnueli. Lecture Notes in Computer Science, vol. 6200, pp. 260–278. Springer (2010)
  * [26] Maler, O., Pnueli, A.: Tight bounds on the complexity of cascaded decomposition of automata. In: Proc. of FOCS. pp. 672–682 (1990)
  * [27] Maler, O., Pnueli, A.: On the cascaded decomposition of automata, its complexity and its application to logic. Unpublished. Available at: http://www-verimag.imag.fr/~maler/Papers/decomp.pdf (1994)
  * [28] Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: PODC. pp. 377–410. ACM (1990)
  * [29] Maretic, G.P., Dashti, M.T., Basin, D.A.: LTL is closed under topological closure. Inf. Process. Lett. 114(8), 408–413 (2014)
  * [30] Markey, N.: Temporal logic with past is exponentially more succinct. Bull. EATCS 79, 122–128 (2003)
  * [31] McNaughton, R., Papert, S.A.: Counter-Free Automata (MIT research monograph no. 65). The MIT Press (1971)
  * [32] Michel, M.: Complementation is more difficult with automata on infinite words. CNET, Paris 15 (1988)
  * [33] Muller, D.E., Saoudi, A., Schupp, P.E.: Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In: Proceedings Third Annual Symposium on Logic in Computer Science. pp. 422–423. IEEE Computer Society (1988)
  * [34] Perrin, D.: Recent results on automata and infinite words. In: International Symposium on Mathematical Foundations of Computer Science. pp. 134–148. Springer (1984)
  * [35] Safra, S.: Complexity of automata on infinite objects. Ph.D. thesis, Weizmann Institute, Rehovot, Israel (1989)
  * [36] Schewe, S.: Büchi Complementation Made Tight. In: Albers, S., Marion, J.Y. (eds.) Proc. of 26th International STACS. Leibniz International Proceedings in Informatics (LIPIcs), vol. 3, pp. 661–672 (2009)
  * [37] Sickert, S., Esparza, J.: An efficient normalisation procedure for linear temporal logic and very weak alternating automata. In: LICS. pp. 831–844. ACM (2020)
  * [38] Thomas, W.: Star-free regular sets of $\omega$-sequences. Information and Control 42(2), 148–156 (1979)
  * [39] Thomas, W.: A combinatorial approach to the theory of $\omega$-automata. Information and Control 48(3), 261–283 (1981)
  * [40] Thomas, W.: Automata on infinite objects. In: Formal Models and Semantics, pp. 133–191. Elsevier (1990)
  * [41] Vardi, M., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. of LICS. pp. 332–344 (1986)
  * [42] Wilke, T.: Classifying discrete temporal properties. In: Annual symposium on theoretical aspects of computer science. pp. 32–46. Springer (1999)
  * [43] Wilke, T.: Past, present, and infinite future. In: 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2016)
  * [44] Wilke, T.: Backward deterministic Büchi automata on infinite words. In: 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2017). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2018)
  * [45] Wolper, P.: Temporal logic can be more expressive 56(1–2), 72–99 (1983)
  * [46] Zuck, L.D.: Past Temporal Logic. Ph.D. thesis, The Weizmann Institute of Science, Israel (Aug 1986)

Open Access This chapter is licensed under the terms of the Creative
CommonsAttribution 4.0 International License
(http://creativecommons.org/licenses/by/4.0/), which permits use, sharing,
adaptation, distribution and reproduction in any medium or format, as long as
you give appropriate credit to the original author(s) and the source, provide
a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the
chapter’s Creative Commons license, unless indicated otherwise in a credit
line to the material. If material is not included in the chapter’s Creative
Commons license and your intendeduse is not permitted by statutory regulation
or exceeds the permitted use, you will need to obtain permission directly from
the copyright holder.

##  Appendix 0.A Omitted Proofs

###  0.A.1 Proofs from Section 3

*

###### Proof.

Consider an LTL formula $\varphi$ and words $w_{i}=(uv^{i}t)$ and
$w_{j}=(uv^{j}t)$, such that $i,j>0pt{\varphi}$. We prove the claim by
induction on the structure of $\varphi$.

Base case: $\varphi$ is an atomic proposition or a Boolean constant. Indeed,
$0pt{\varphi}=0$ and we have that $w_{i}\models\varphi$ iff
$w_{j}\models\varphi$, because the first letter of these two words, which is
the first letter of $u$ if $u$ is not empty and the first letter of $v$
otherwise, is the same.

Induction step: We assume that the claim holds for all strict subformulas of
$\varphi$. Let $\psi_{1}$ and $\psi_{2}$ be strict subformulas of $\varphi$.
We show that the claim holds for:

  * •

$\varphi=\neg\psi_{1}$: Since $0pt{\varphi}=0pt{\psi_{1}}$, it follows that
$i,j>0pt{\psi_{1}}$, and therefore by the induction assumption
$w_{i}\models\psi_{1}$ iff $w_{j}\models\psi_{1}$, implying that
$w_{i}\models\varphi$ iff $w_{j}\models\varphi$.

  * •

$\varphi=\psi_{1}\land\psi_{2}$: Since
$0pt{\varphi}=\max(0pt{\psi_{1}},0pt{\psi_{2}})$, it follows that
$i,j>0pt{\psi_{1}}$ and $i,j>0pt{\psi_{2}}$. Therefore by the induction
assumption ($w_{i}\models\psi_{1}$ iff $w_{j}\models\psi_{1}$) and
($w_{i}\models\psi_{2}$ iff $w_{j}\models\psi_{2}$). Hence,
$w_{i}\models\psi_{1}\land\psi_{2}$ iff $w_{j}\models\psi_{1}\land\psi_{2}$.

  * •

$\varphi={\mathbf{X}}\psi_{1}$: Recall that a word $w$ satisfies $\varphi$ iff
$w^{1}$ satisfies $\psi_{1}$. Observe that $w_{i}^{1}=u^{\prime}v^{i-1}t$ and
$w_{j}^{1}=u^{\prime}v^{j-1}t$, where $u^{\prime}=(uv)^{1}$. Since
$0pt{\psi_{1}}=0pt{\varphi}-1$, it follows that $i-1,j-1>0pt{\psi_{1}}$.
Hence, by the induction assumption $w_{i}^{1}\models\psi_{1}$ iff
$w_{j}^{1}\models\psi_{1}$, and therefore $w_{i}\models\varphi$ iff
$w_{j}\models\varphi$.

  * •

$\varphi=\psi_{1}{\mathbf{U}}\psi_{2}$: We will show that if $w_{i}$ satisfies
$\varphi$ then so does $w_{j}$.

If $w_{i}$ satisfies $\varphi$ then there is a position $p$ of $w_{i}$, such
that $w_{i}^{p}\models\psi_{2}$ and for every $k<p$,
$w_{i}^{k}\models\psi_{1}$. Let $o$ be the position of $w_{i}$ that appears at
the beginning of the $v$-block that is $0pt{\varphi}$ blocks of $v$ before the
$t$ part of $w_{i}$, namely $o=|uv^{i-0pt{\varphi}}|$. (See Figure 2.)

$\cdots$$v$$w_{i}:$$u$$v$$v$$t$$v$$o$$0$or more blocks of
$v$$0pt{\varphi}$blocks of $v$

Figure 2: The structure of the word $w_{i}$ from the proof of Section 3.

We split the proof into disjoint cases, depending on the location of $p$
within $w_{i}$.

    * –

$p<|u|$: Let $u^{\prime}$ be the infix of $w_{j}$ from $p$ to the end of $u$,
namely $u^{\prime}=w_{i}[p..|u|-1]$. Then $w_{i}^{p}=u^{\prime}v^{i}t$ and
$w_{j}^{p}=u^{\prime}v^{j}t$. Since $i,j>0pt{\varphi}>0pt{\psi_{2}}$, by the
induction assumption $w_{i}^{p}\models\psi_{2}$ iff $w_{j}^{p}\models\psi_{2}$
and therefore $w_{j}^{p}\models\psi_{2}$. Likewise, since
$i,j>0pt{\varphi}>0pt{\psi_{1}}$, by the induction assumption for every
position $m<p$, $w_{i}^{m}\models\psi_{1}$ iff $w_{j}^{m}\models\psi_{1}$ and
therefore $w_{j}^{m}\models\psi_{1}$.

    * –

$p\in[|u|..o-1]$: Let $p^{\prime}$ be the position in $w_{j}$ that appears in
the first $v$-block after $u$ and that is located within that $v$-block like
$p$ is located within its $v$-block. That is,
$p^{\prime}=|u|+((p-|u|)\mod|v|)$. Let $u^{\prime}$ be the remaining suffix in
the $v$-block of $p$ and $p^{\prime}$, that is
$u^{\prime}=w_{j}[p^{\prime}+1..|u|+|v|]$. Let $h$ be the number of $v$-blocks
that appear after $p$ and before the $t$ part of $w_{i}$, that is
$h=0pt{\varphi}+\lfloor(o-p)/|v|\rfloor$. Then $w_{i}^{p}=u^{\prime}v^{h}t$
and $w_{j}^{p^{\prime}}=u^{\prime}v^{j-1}t$. Since $h\geq
0pt{\varphi}>0pt{\psi_{2}}$ and $j-1\geq 0pt{\varphi}>0pt{\psi_{2}}$, we have
by the induction assumption that $w_{j}^{p^{\prime}}\models\psi_{2}$ iff
$w_{i}^{p}\models\psi_{2}$, and therefore $w_{j}^{p^{\prime}}\models\psi_{2}$.

Now, for every position $m<p^{\prime}$, let $u^{\prime}$ be the infix of
$w_{j}$ from $m$ to the end of the first $v$-block of $w_{j}$, that is
$u^{\prime}=w_{j}[m..|u|+|v|]$. Then $w_{i}^{m}=u^{\prime}v^{i-1}t$ and
$w_{j}^{m}=u^{\prime}v^{j-1}t$. Since $i-1>0pt{\psi_{1}}$ and
$j-1>0pt{\psi_{1}}$, by the induction assumption $w_{i}^{m}\models\psi_{1}$
iff $w_{j}^{m}\models\psi_{1}$ and therefore $w_{j}^{m}\models\psi_{1}$.

    * –

$p\geq o$: Let $p^{\prime}$ and $o^{\prime}$ be the positions in $w_{j}$ that
are at the same distance from the $t$ part of $w_{j}$ as $p$ and $o$ are from
the $t$ part $w_{i}$, namely $o^{\prime}=|uv^{j-0pt{\varphi}}|$ and
$p^{\prime}=o^{\prime}+(p-o)$. Observe that $w_{i}^{o}=w_{j}^{o^{\prime}}$ and
$w_{j}^{p^{\prime}}=w_{i}^{p}$, implying that
$w_{j}^{p^{\prime}}\models\psi_{2}$.

Further, for every position $m\in[o-|v|..p]$ of $w_{i}$, let $m^{\prime}$ be
the corresponding position in $w_{j}$, namely $m^{\prime}=o^{\prime}+(m-o)$.
Then $w_{j}^{m^{\prime}}=w_{i}^{m}$, and accordingly
$w_{j}^{m^{\prime}}\models\psi_{1}$.

Now, for every position $m^{\prime}\in[|u|..o-|v|-1]$, we have by the
induction assumption that $w_{j}^{m^{\prime}}\models\psi_{1}$ iff
$w_{j}^{m^{\prime}+|v|}\models\psi_{1}$ (as both words have the same prefix
until the end of the first $v$ block, followed by at least $0pt{\psi_{1}}+1$
blocks of $v$ and then $t$), implying that
$w_{j}^{m^{\prime}}\models\psi_{1}$.

Finally, for every position $m\in[0..|u|-1]$, we have by the induction
assumption that $w_{i}^{m}\models\psi_{1}$ iff $w_{j}^{m}\models\psi_{1}$,
implying that $w_{j}^{m}\models\psi_{1}$.

∎

*

###### Proof.

Let $\\#=\\{p\\}$ be the shorthand for a new atomic proposition $p$. Given a
unary LTL formula recognising $L\subseteq\\{a\\}^{+}$, it can be turned into a
general LTL formula of linear length that recognises
$L^{\prime}=\\{v\\#^{\omega}\mid v\in L\\}$ over the alphabet
$\Sigma^{\prime}=2^{\\{p\\}}$. Then, the statement is a direct consequence of
Section 3. ∎

*

###### Proof.

The very weak deterministic automaton for $L$ consists of $n+2$ states
$\\{0,\dots,n+1\\}$, with an $a$-transition from state $i$ to state $i+1$ and
a self loop at state $n+1$. The state $i$ is accepting whenever $a^{i}\in L$.
∎

*

###### Proof.

Deterministic automata: For the upper bound, consider a DFA ${\cal A}$
recognising an LTL definable language. By a pumping argument, if $w\in L({\cal
A})$ for some $w$ longer than $n$, then $L({\cal A})$ is infinite. Considering
the dual automaton ${\cal A}^{\prime}$ of ${\cal A}$, recognising the
complement language, by the pumping argument if $w\not\in L({\cal A})$ for
some $w$ longer than $n$, then the complement of $L({\cal A})$ is infinite.
Hence, by Section 3, $L({\cal A})$ agrees on all words of length more than
$n$, and by Section 3 there is an LTL formula for it of length in $O(n)$. As
for the lower bound, since there is a DFA of size $n$ recognising ${a^{k}}$,
it directly follows from Section 3.

Nondeterministic automata: Directly follows from Sections 3 and 3.

Alternating automata: Directly follows from Figs. 1 and 2. ∎

*

###### Proof.

First recall that the run of an alternating automaton is a tree, of which all
paths are accepting if and only if the run itself is accepting. These runs can
be pumped in the same way as runs of nondeterministic automata, except that
the run to be pumped must be of length over $2^{n}$ to guarantee that the set
of states in a cross-section of the run are repeated.

Then, by a pumping argument, if $w\in L({\cal A})$ for some $w$ longer than
$2^{n}$, then $L({\cal A})$ is infinite: indeed, let ${\cal A}^{\prime}$ be an
NFA equivalent to ${\cal A}$ of size at most $2^{n}$; if ${\cal A}^{\prime}$
accepts a word longer than $2^{n}$, then its run sees some state more than
once and can be pumped to build infinitely many accepting runs. Dually, since
AFA are easy to complement, if $w^{\prime}\notin L({\cal A})$ for some
$w^{\prime}$ longer than $2^{n}$, then $\Sigma^{*}\setminus L({\cal A})$ is
infinite. The existence of both $w\in L({\cal A})$ and $w^{\prime}\notin
L({\cal A})$ longer than $2^{n}$ therefore contradicts Lemma 3. We conclude
that $L(A)$ agrees on all words of length over $2^{n}$. Thus, by Section 3
there is an LTL formula for $L({\cal A})$ of length in $O(2^{n})$. ∎

*

###### Proof.

The idea of the construction is that it represents an $n$-bit up-counter,
having two states for each bit, one corresponding to $1$, one to $0$ (see Fig.
1).

Given a way to resolve the nondeterministic choices, the resulting set of
“active” states of the automaton represents a configuration of the counter:
The nondeterminism in each bit-state chooses whether to change the bit’s value
(going left in Fig. 1), in which case the universality ensures that all lower
bits are set to $0$, or to preserve the bit’s value (going right in Fig. 1),
in which case the universality ensures that at least one lower bit is set to
$1$.

The automaton thus preserves the invariant that a correct update (for example
from $011$ to $100$) ensures that the number of active states is constant, in
particular, if all updates are correct, then exactly one state per bit is
active at a time; an incorrect update on the other hand increases the number
of active states. The set of accepting states corresponds to the bit-
configuration for $2^{n-1}$, where a transition to a state $q_{i,\mathbf{0}}$,
for every $i<n$, can be changed to a move to $q_{acc}$, provided that it is on
the last letter of the input word. (There is no transition out of $q_{acc}$).
The only way to build an accepting run is to correctly update the counter at
each step; an incorrect update ensures that both states of some bit are set
from thereon, of which one must be rejecting.

As for the automaton size, which is the number of subformulas in the
transition function, observe that it is linear in $n$, since there are $2n$
states and the total number of subformulas in the transition function is as
follows: The transition functions of $q_{1,\mathbf{0}}$ and $q_{1,\mathbf{1}}$
have together four subformulas, and the transition function of every other
state $q_{(i,\cdot)}$ adds up to $4$ subformulas: (i) the topmost disjunction
of whether to change the bit’s value or not; (ii)&(iii) the universality
involved in each of these two options; and (iv) within each of the two
universality subformulas – a disjunction or conjunction between
$q_{(i-1,\cdot)}$ and $(q_{(i-1,\cdot)},\ldots,q_{(i-1,\cdot)})$, where the
latter subformula (within the parenthesis) is already used in the transition
function of $q_{(i-1,\cdot)}$ and these two formulas (one of conjunction and
one of disjunction) is used by both $q_{i,\mathbf{0}}$ and $q_{i,\mathbf{1}}$
(except for $q_{n,\mathbf{1}}=q_{acc}$, which has no outgoing transitions). ∎

*

###### Proof.

If $L({\cal A})$ is finite, then by a pumping argument, ${\cal A}$ only
accepts words up to length $n$, and by Section 3 we are done. We consider co-
finite $L({\cal A})$.

We will argue using 2-way deterministic automata, which are deterministic
automata that process words of the form $\vdash\\!\\!w\\!\\!\dashv$, where
$\vdash$ and $\dashv$ are start- and end-of-word markers respectively, and
where transitions specify whether to read the letter to the right or to the
left of the current position. They accept by reaching an end state, and reject
by reaching a rejecting state or by failing to terminate. For a more formal
definition, see [17]. We will use the facts that a unary NFA can be turned
into a 2-way DFA of size $O(n^{2})$ [9], that a 2-way DFA of size $m$ can be
complemented into one of size $4m$ [17], and that the smallest 2-way DFA
recognising $\\{a^{k}\\}$ is of length $k+2$ [1].

The NFA ${\cal A}$ can be turned into a 2-way DFA ${\cal D}$ with $O(n^{2})$
states recognising the same language. From ${\cal D}$, we can obtain a 2-way
DFA ${\cal D}^{\prime}$ that recognises $a^{*}\setminus\\{a^{k}\\}$, where
$a^{k}$ is the longest word not in $L({\cal A})$, as follows: we keep the
states and transitions involved in the run of ${\cal D}$ on
$\vdash\\!\\!a^{k}\\!\\!\dashv$, which is rejecting and must read $\dashv$
(since, by the co-finiteness of $L({\cal A})$, there are accepted words longer
than $a^{k}$). Notice that states in ${\cal D}^{\prime}$ may have only some of
the transitions they had in ${\cal D}$ – only those that are involved in the
run on $a^{k}$. We then add an $a$-transition and a $\dashv$-transition from
all states without such transitions, and these all lead to the (accepting) end
state.

Notice that ${\cal D}^{\prime}$ is still deterministic and not larger than
${\cal D}$. It still rejects $a^{k}$, on which it has the same run as ${\cal
D}$, but accepts all other words, which are either shorter than $a^{k}$ and
therefore accepted via one of the new $\dashv$-transitions, or are longer than
$a^{k}$ and accepted when they read the $k+1^{th}$ letter.

We can then complement ${\cal D}^{\prime}$ into a 2-way DFA ${\cal
D}^{\prime\prime}$ of size linear in the size of $D^{\prime}$, namely in
$O(n^{2})$, that recognises $\\{a^{k}\\}$. However, since ${\cal
D}^{\prime\prime}$ must be of size at least $k+2$, we get that $k+2$ is at
most in $O(n^{2})$, meaning that the longest word rejected by ${\cal A}$,
which is of length $k$, is of length in $O(n^{2})$.

Then, there is an equivalent very weak automaton of the size of the longest
word not in $L({\cal A})$, from Section 3. ∎

###  0.A.2 Proofs from Section 4.1

*

###### Proof.

We provide the proof for Rabin automata. The proofs for Büchi and coBüchi
automata are special cases of the Rabin case.

Let ${\cal D}=(\Sigma,Q,\iota,\delta,\alpha)$, and $h$ be the mapping via
which $(\Sigma,Q,\delta)$ is homomorphic to ${\cal A}$. We shall define a
configuration $\iota^{\prime}$ of ${\cal A}$, and a set $\alpha^{\prime}$ of
pairs of sets of configurations of ${\cal A}$ that will provide the initial
state and acceptance condition of ${\cal D}^{\prime}$, making it equivalent to
${\cal D}$.

For the initial state of ${\cal D}^{\prime}$, one can choose any configuration
$\iota^{\prime}\in h^{-1}(\iota)$: A run of ${\cal A}$ starting in
$\iota^{\prime}$ corresponds via $h$ to a run of ${\cal D}$ starting in
$h(\iota^{\prime})=\iota$.

As for the acceptance condition, consider the run $r^{\prime}$ of ${\cal
D}^{\prime}$ on a word $w$, starting in $\iota^{\prime}$, and let
$r=h(r^{\prime})$ be the corresponding run of ${\cal D}$ on $w$. (With
$h(r^{\prime})$, we mean the sequence of states of ${\cal D}$, obtained by
mapping with $h$ each configuration of $r^{\prime}$.) Then, $r^{\prime}$
should be accepting iff $r$ is.

Recall that $r$ is accepting iff $\it inf(r)\cap G\neq\emptyset$ and $\it
inf(r)\cap B=\emptyset$ for some pair $(G,B)\in\alpha$. Hence, $r^{\prime}$
should be accepting “according to $(G,B)$” iff $h(\it inf(r^{\prime}))\cap
G\neq\emptyset$ and $h(\it inf(r^{\prime}))\cap B=\emptyset$.

Thus, $r^{\prime}$ should visit infinitely often some configuration in
$G^{\prime}=h^{-1}(G)$ and finitely often every configuration in
$B^{\prime}=h^{-1}(B)$. Hence, there are $k$ acceptance pairs
$(G^{\prime},B^{\prime})$ in $\alpha^{\prime}$, each corresponding to an
acceptance pair $(G,B)$ in ${\cal D}$. ∎

*

###### Proof.

Let ${\cal D}=(\Sigma,Q,\iota,\delta,\alpha)$, and $h$ be the mapping via
which $(\Sigma,Q,\delta)$ is homomorphic to ${\cal A}$. We shall define a
configuration $\iota^{\prime}$ of ${\cal A}$, and a set $\alpha^{\prime}$ of
sets of configurations of ${\cal A}$ that will provide the initial state and
acceptance condition of ${\cal D}^{\prime}$, making it equivalent to ${\cal
D}$.

For the initial state of ${\cal D}^{\prime}$, one can choose any configuration
$\iota^{\prime}\in h^{-1}(\iota)$: A run of ${\cal A}$ starting in
$\iota^{\prime}$ corresponds via $h$ to a run in ${\cal D}$ starting in
$h(\iota^{\prime})=\iota$.

As for the acceptance condition, consider the run $r^{\prime}$ of ${\cal
D}^{\prime}$ on $w$, starting in $\iota^{\prime}$, and let $r=h(r^{\prime})$
be the run of ${\cal D}$ on $w$ (that is defined by mapping each configuration
of $r^{\prime}$ to a state of ${\cal D}$ via $h$). Then, $r^{\prime}$ should
be accepting iff $r$ is.

Recall that $r$ is accepting iff $\it inf(r)=M$, for some $M=\\{q_{1},\ldots
q_{l}\\}\in\alpha$. Hence, $r^{\prime}$ should be accepting “according to $M$”
iff $h(\it inf(r^{\prime}))=M$. Thus, $r^{\prime}$ should visit finitely often
every configuration in $h^{-1}(Q\setminus M)$, and for _every_ $i\in[1..l]$,
visit _some_ configurations in $G_{i}=h^{-1}(q_{i})$ infinitely often.

Since we should consider every choice of configurations in
$G_{i}=h^{-1}(q_{i})$, where $|G_{i}|\leq m$, there are up to $2^{m}$ choices
for $G_{i}$, and therefore up to $(2^{m})^{n}$ choices for $M$, each providing
a Muller set $G$ of configurations to be visited infinitely often.

As there are up to $2^{n}$ sets in $\alpha$, we end up with up to
$2^{n}(2^{m})^{n}\in 2^{O(mn)}$ sets in $\alpha^{\prime}$. ∎

###  0.A.3 Proofs from Section 4.2

*

###### Proof.

Observe first that there is no circularity in the definitions of the five
reachability formulas, even though they are defined by each other: Formula 2
is defined on top of formula 1, which is defined on top of formulas 3 and 5,
while formulas 3, 4, and 5 are defined with respect to reachability formulas
over configurations of a lower level.

We prove the statement by induction on the level $m$ of the configurations
$S$, $B$, $T$ in the reachability formulas. We split the proof to five cases
corresponding to the five reachability formulas in Table 1. In order to
clarify which equivalence of the induction hypothesis is used we denote by
(I.H.1) the equivalence in Table 1 for reachability formula 1, (I.H.2) the
equivalence for reachability formula 2, and so on.

Reachability formula 1

($m=0$): There is exactly one configuration of level $0$ and it is the empty
configuration. Thus $S=T=B=\langle\rangle$. We then derive:

$\begin{array}[]{cl}&w\models\langle\rangle\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle\rangle(\beta)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle\rangle(\beta)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle\rangle(\beta)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle\rangle(\beta)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptscriptstyle{}}}\langle\rangle\left(\tau\right)\\\\[8.99994pt]
\iff&w\models(\neg\beta){\mathbf{U}}\tau\\\\[6.00006pt] \iff&\exists i\geq
0.\leavevmode\nobreak\ w_{[i..]}\models\tau\land\forall
j\in[0..i).\leavevmode\nobreak\ w_{[j..]}\not\models\beta\\\\[6.00006pt]
\iff&\exists i\geq 0.\leavevmode\nobreak\
\delta(\langle\rangle,w_{[0..i)})=\langle\rangle\land w_{[i..]}\models\tau\\\
&\qquad\qquad\land\leavevmode\nobreak\ \forall j\in[0..i).\leavevmode\nobreak\
\delta(\langle\rangle,w_{[0..j)})\neq\langle\rangle\lor
w_{[j..]}\not\models\beta\end{array}$

($m\rightarrow m+1$): Let $\langle S,s\rangle,\langle T,t\rangle,\langle
B,b\rangle\in Q_{1}\times\cdots\times Q_{m+1}$ be arbitrary configurations of
level $m+1$. Thus we can use the equalities from Table 1 for all
configurations of $Q_{1}\times\cdots\times Q_{m}$ as induction hypotheses. We
need to show that:

$\begin{array}[]{cl}&w\models\langle
S,s\rangle\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle(\beta)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle(\beta)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle(\beta)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle(\beta)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa 04B}\\!\\!\scriptscriptstyle{}}}\langle
T,t\rangle\left(\tau\right)\\\\[8.99994pt] \iff&w\models\langle
S,s\rangle\xrightarrow[\bcancel{\langle
B,b\rangle\left(\beta\right)}]{}\langle T,t\rangle\left(\tau\right)\lor\langle
S,s\rangle\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\dabar@\dabar@\dabar@\dabar@}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle\left(\beta\right)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\dabar@\dabar@\dabar@\dabar@}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle\left(\beta\right)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\dabar@\dabar@\dabar@\dabar@}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle\left(\beta\right)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\dabar@\dabar@\dabar@\dabar@}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle\left(\beta\right)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa 04B}\\!\\!\scriptscriptstyle{}}}\langle
T,t\rangle\left(\tau\right)\\\\[8.99994pt] \iff&\exists i\geq
0.\leavevmode\nobreak\ \delta(\langle S,s\rangle,w_{[0..i)})=\langle
T,t\rangle\land w_{[i..]}\models\tau\\\ &\qquad\qquad\land\leavevmode\nobreak\
(\forall j\in[0..i).\leavevmode\nobreak\ \delta(\langle
S,s\rangle,w_{[0..j)})\neq\langle B,b\rangle\lor
w_{[j..]}\not\models\beta)\end{array}$

We split this into the ($\Rightarrow$)- and ($\Leftarrow$)-direction:

($\Rightarrow$): We further refine this and first assume that the first
disjunct is satisfied by $w$ and defer the other case to a later point in the
proof. We then apply (I.H.3) and derive:

$\begin{array}[]{cl}&w\models\langle S,s\rangle\xrightarrow[\bcancel{\langle
B,b\rangle\left(\beta\right)}]{}\langle
T,t\rangle\left(\tau\right)\\\\[8.99994pt] \iff&\exists i\geq
0.\leavevmode\nobreak\ \delta(\langle S,s\rangle,w_{[0..i)})=\langle
T,t\rangle\land w_{[i..]}\models\tau\\\ &\qquad\qquad\land\leavevmode\nobreak\
(\forall j\in[0..i).\leavevmode\nobreak\ \delta(\langle
S,s\rangle,w_{[0..j)})\neq\langle B,b\rangle\lor w_{[j..]}\not\models\beta)\\\
&\qquad\qquad\land\leavevmode\nobreak\ (\forall
j\in[0..i).\leavevmode\nobreak\ \langle
w[j],\delta(S,w_{[0..j)})\rangle\in\mathsf{Stay}(s))\\\ \implies&\exists i\geq
0.\leavevmode\nobreak\ \delta(\langle S,s\rangle,w_{[0..i)})=\langle
T,t\rangle\land w_{[i..]}\models\tau\\\ &\qquad\qquad\land\leavevmode\nobreak\
(\forall j\in[0..i).\leavevmode\nobreak\ \delta(\langle
S,s\rangle,w_{[0..j)})\neq\langle B,b\rangle\lor
w_{[j..]}\not\models\beta)\end{array}$

We now assume that the first disjunct is _not_ satisfied by $w$ and thus the
second disjunct is satisfied by $w$. We then derive using (I.H.5):

$\begin{array}[]{cl}&w\models\langle
S,s\rangle\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\dabar@\dabar@\dabar@\dabar@}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle\left(\beta\right)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\dabar@\dabar@\dabar@\dabar@}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle\left(\beta\right)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\dabar@\dabar@\dabar@\dabar@}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle\left(\beta\right)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\dabar@\dabar@\dabar@\dabar@}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle\left(\beta\right)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa 04B}\\!\\!\scriptscriptstyle{}}}\langle
T,t\rangle\left(\tau\right)\\\\[8.99994pt] \iff&\exists i_{1},i_{2}\geq
0.\leavevmode\nobreak\ \delta(\langle S,s\rangle,w_{[0..i_{1})})=\langle
T,t\rangle\land w_{[i_{1}..]}\models\tau\\\
&\qquad\qquad\land\leavevmode\nobreak\ (\exists
j_{1}\in[0..i_{1}).\leavevmode\nobreak\ \langle
w[j_{1}],\delta(S,w_{[0..j_{1})})\rangle\in\mathsf{Enter}(t)\\\
&\qquad\qquad\land\leavevmode\nobreak\ \langle
w[i_{2}],\delta(S,w_{[0..i_{2})})\rangle\in\mathsf{Leave}(s)\\\
&\qquad\qquad\land\leavevmode\nobreak\ (\forall
j\in[0..\max(i_{1}{-}1,i_{2})].\leavevmode\nobreak\ \delta(\langle
S,s\rangle,w_{[0..j)})\neq\langle B,b\rangle\lor w_{[j..]}\not\models\beta)\\\
\implies&\exists i\geq 0.\leavevmode\nobreak\ \delta(\langle
S,s\rangle,w_{[0..i)})=\langle T,t\rangle\land w_{[i..]}\models\tau\\\
&\qquad\qquad\land\leavevmode\nobreak\ (\forall
j\in[0..i).\leavevmode\nobreak\ \delta(\langle
S,s\rangle,w_{[0..j)})\neq\langle B,b\rangle\lor
w_{[j..]}\not\models\beta)\end{array}$

($\Leftarrow$): We assume that $w$ satisfies the right-hand side of the
equation and we instantiate $i$ to be the smallest non-negative integer such
that:

$\begin{array}[]{cl}&\delta(\langle S,s\rangle,w_{[0..i)})=\langle
T,t\rangle\land w_{[i..]}\models\tau\\\ &\qquad\qquad\land\leavevmode\nobreak\
(\forall j\in[0..i).\leavevmode\nobreak\ \delta(\langle
S,s\rangle,w_{[0..j)})\neq\langle B,b\rangle\lor
w_{[j..]}\not\models\beta)\end{array}$

Assume that for all proper prefixes of $w_{[0..i)}$ the combined letter stays
in $s$, i.e., $\langle w[j],\delta(S,w_{[0..j)})\rangle\in\mathsf{Stay}(s)$
for all $j\in[0..i)$. We then apply (I.H.3) and obtain that $w$ satisfies
$\langle S,s\rangle\xrightarrow[\bcancel{\langle
B,b\rangle\left(\beta\right)}]{}\langle T,t\rangle\left(\tau\right)$ and so
the left-hand side of the equation is satisfied by $w$. Thus let $k\in[0..i)$
be the smallest non-negative integer such that:

$\langle w[k],\delta(S,w_{[0..k)})\rangle\in\mathsf{Leave}(s)$

Since $k<i$, we immediately obtain one of the missing preconditions for
applying (I.H.5):

$\forall j_{2}\in[0..k].\leavevmode\nobreak\ \delta(\langle
S,s\rangle,w_{[0..j_{2})})\neq\langle B,b\rangle\lor
w_{[j_{2}..]}\not\models\beta$

The second missing precondition is that we need to find a $j_{1}\in[0..i)$
such that $\langle
w[j_{1}],\delta(S,w_{[0..j_{1})})\rangle\in\mathsf{Enter}(t)$: In the case
$s\neq t$ this is straightforward, since after reading $w_{[0..i)}$ we reach
$\langle T,t\rangle$, and thus there must be a $j_{1}<i$ such that $\langle
w[j_{1}],\delta(S,w_{[0..j_{1})})\rangle\in\mathsf{Enter}(t)$. Thus let us
assume $s=t$. In general there might be not such an index $j_{1}$. However, we
have shown that $\langle w[k],\delta(S,w_{[0..k)})\rangle\in\mathsf{Leave}(s)$
for some $k<i$ and by the same reasoning as above there must be $j_{1}$
between $k$ and $i$ such that $\langle
w[j_{1}],\delta(S,w_{[0..j_{1})})\rangle\in\mathsf{Enter}(t)$.

We now can apply (I.H.5) and conclude this direction of the proof.

Reachability formula 2

We proceed by a straightforward derivation for which we use (I.H.1) in the
second step:

$\begin{array}[]{cl}&w\models
S\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{B(\beta)}$}}^{\hbox{\set@color$\scriptstyle\,\text{\tiny
weak}$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{B(\beta)}$}}^{\hbox{\set@color$\scriptstyle\,\text{\tiny
weak}$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{B(\beta)}$}}^{\hbox{\set@color$\scriptstyle\,\text{\tiny
weak}$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{B(\beta)}$}}^{\hbox{\set@color$\scriptstyle\,\text{\tiny
weak}$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\scriptscriptstyle{}}}T\left(\tau\right)\\\\[8.99994pt]
\iff&w\not\models
S\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{T(\tau)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{T(\tau)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{T(\tau)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{T(\tau)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptscriptstyle{}}}B\left(\beta\right)\\\\[8.99994pt]
\iff&\neg\big{(}\exists i\geq 0.\leavevmode\nobreak\
\delta(S,w_{[0..i)})=B\land w_{[i..]}\models\beta\\\
&\qquad\qquad\land\leavevmode\nobreak\ (\forall
j\in[0..i).\leavevmode\nobreak\ \delta(S,w_{[0..j)})\neq T\lor
w_{[j..]}\not\models\tau)\big{)}\\\ \iff&\forall i\geq 0.\leavevmode\nobreak\
(\delta(S,w_{[0..i)})=B\land w_{[i..]}\models\beta)\\\
&\qquad\qquad\rightarrow\leavevmode\nobreak\ (\exists
j\in[0..i).\leavevmode\nobreak\ \delta(S,w_{[0..j)})=T\land
w_{[j..]}\models\tau)\end{array}$

Reachability formula 3

We want to prove the following equivalence:

$\begin{array}[]{cl}&w\models\langle S,s\rangle\xrightarrow[\bcancel{\langle
B,b\rangle\left(\beta\right)}]{}\langle T,t\rangle\left(\tau\right)\\\
\iff&\exists i\geq 0.\leavevmode\nobreak\ \delta(\langle
S,s\rangle,w_{[0..i)})=\langle T,t\rangle\land w_{[i..]}\models\tau\\\
&\qquad\qquad\land\leavevmode\nobreak\ (\forall
j_{1}\in[0..i).\leavevmode\nobreak\ \delta(\langle
S,s\rangle,w_{[0..j_{1})})\neq\langle B,b\rangle\lor
w_{[j_{1}..]}\not\models\beta)\\\ &\qquad\qquad\land\leavevmode\nobreak\
(\forall j_{2}\in[0..i).\leavevmode\nobreak\ \langle
w[j_{2}],\delta(S,w_{[0..j_{2})})\rangle\in\mathsf{Stay}(s))\end{array}$

($\Rightarrow$): Assume that $w$ satisfies the left-hand side of the
equivalence. Notice that if $w$ does not satisfy $\varphi\coloneqq\langle
S,s\rangle\xrightarrow[\bcancel{\langle
B,b\rangle\left(\beta\right)}]{>0}\langle T,t\rangle\left(\tau\right)$, then
necessarily $\delta(\langle S,s\rangle,w_{[0..0)})=\langle T,t\rangle$ and
$w_{[0..]}\models\tau$ and thus the right-hand side trivially holds for $i=0$.

Thus we can assume that $w$ satisfies $\varphi$ and using the same reasoning
we know that either $\delta(\langle S,s\rangle,w_{[0..0)})=\langle B,b\rangle$
or $w_{[0..]}\models\beta$ does not hold, which takes care of the case
$j_{1}=0$ in the second line of the right-hand side, assuming $i>0$.

Since we have $w\models\varphi$, there must be a
$\langle\sigma,T^{\prime}\rangle\in\mathsf{Stay}(s)$ with $\delta(\langle
T^{\prime},s\rangle,\sigma)=\langle T,t\rangle$ such that the matching
disjunct $\psi$ of $\varphi$ is satisfied by $w$. Note that this immediately
implies that $s=t$. Observe that $\psi$ is a conjunction of formulas with the
shape

$S\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\cdot(\cdot)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\cdot(\cdot)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\cdot(\cdot)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\cdot(\cdot)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptscriptstyle{}}}T^{\prime}\left(\sigma\land{\mathbf{X}}\tau\right)$

and we now apply (I.H.1) to all reachability formulas. Since they all share
the same target, we can instantiate them to the same $i^{\prime}$ (where
$i^{\prime}$ is the smallest non-negative integer satisfying the conditions)
such that:

  1. (a)

$\delta(S,w_{[0..i^{\prime})})=T^{\prime}$

  2. (b)

$w[i^{\prime}]=\sigma$

  3. (c)

$w_{[i^{\prime}+1..]}\models\tau$

  4. (d)

For every $\langle\eta,L\rangle\in\mathsf{Leave}(s)$ and every
$j\in[0..i^{\prime})$ at least one of the following statements holds:

    1. (i)

$\delta(S,w_{[0..j)})\neq L$

    2. (ii)

$w[j]\neq\eta$

  5. (e)

For every $\langle\rho,B^{\prime}\rangle\in\mathsf{Stay}(s)$ such that
$\delta(\langle B^{\prime},s\rangle,\rho)=\langle B,b\rangle$ and every
$j\in[0..i^{\prime})$ at least one of the following statements holds:

    1. (i)

$\delta(S,w_{[0..j)})\neq B^{\prime}$

    2. (ii)

$w[j]\neq\rho$

    3. (iii)

$w_{[j+1..]}\not\models\beta$

We now instantiate $i$ of the right-hand side with $i^{\prime}+1$. Remember
that we have $\langle\sigma,T^{\prime}\rangle\in\mathsf{Stay}(s)$ and together
with (a-c) we obtain the first conjunct of the right hand side.

We now establish the third conjunct. Note that for every
$j_{2}\in[0..i^{\prime})$ we have $\langle w[j_{2}],\delta(\langle
S,s\rangle,w_{[0..j_{2})})\rangle\in\mathsf{Stay}(s)$, since
$\mathsf{Stay}(s)=(\Sigma\times Q_{1}\times\cdots\times
Q_{m})\setminus\mathsf{Leave}(s)$ and by (d) we do not encounter an element of
$\mathsf{Leave}(s)$ for any $j_{2}$. Further, for $j_{2}=i^{\prime}$ we obtain
$\langle w[j_{2}],\delta(\langle
S,s\rangle,w_{[0..j_{2})})\rangle\in\mathsf{Stay}(s)$ from (a,b) and the
choice of $\langle\sigma,T^{\prime}\rangle\in\mathsf{Stay}(s)$.

For the second conjunct it remains to show that for every $j_{1}\in[0..i)$:

$\delta(\langle S,s\rangle,w_{[0..j_{1})})\neq\langle B,b\rangle\lor
w_{[j_{1}..]}\not\models\beta$

Assume that $\delta(\langle S,s\rangle,w_{[0..j_{1})})=\langle B,b\rangle$ (if
this is not the case we are immediately done). Due to the already established
third conjunct, we have $\langle
w[j_{1}-1],\delta(S,w_{[0..j_{1}-1)})\rangle=\langle\rho,B^{\prime}\rangle\in\mathsf{Stay}(s)$
and $\delta(\langle B^{\prime},s\rangle,\rho)=\langle B,b\rangle$. Thus (e,i)
and (e,ii) cannot hold and (e,iii) must hold for $j_{1}(=j+1)$.

($\Leftarrow$): We assume that $w$ satisfies the right-hand side and
instantiate $i$ as the smallest $i\geq 0$ such that:

  1. (a)

$\delta(\langle S,s\rangle,w_{[0..i)})=\langle T,t\rangle$

  2. (b)

$w_{[i..]}\models\tau$

  3. (c)

$\forall j\in[0..i).\leavevmode\nobreak\ \delta(\langle
S,s\rangle,w_{[0..j)})\neq\langle B,b\rangle\lor w_{[j..]}\not\models\beta$

  4. (d)

$\forall j\in[0..i).\leavevmode\nobreak\ \langle
w[j],\delta(S,w_{[0..j)})\rangle\in\mathsf{Stay}(s)$

If $i=0$, then due to (a-b) we have immediately $w\models\langle
S,s\rangle\xrightarrow[\bcancel{\langle
B,b\rangle\left(\beta\right)}]{}\langle T,t\rangle\left(\tau\right)$. Thus
without loss of generality we can assume $i>0$ from now on. Further, due to
(c) we have that either $\langle S,s\rangle\neq\langle B,b\rangle$ or
$w\not\models\beta$. Thus it remains to show that $w\models\langle
S,s\rangle\xrightarrow[\bcancel{\langle
B,b\rangle\left(\beta\right)}]{>0}\langle T,t\rangle\left(\tau\right)$. Define
$\sigma$ as $w[i-1]$ and $T^{\prime}$ as $\delta(S,w_{[0..i-1)})$. From (a,d)
we then follow:

  1. (e)

$\langle\sigma,T^{\prime}\rangle\in\mathsf{Stay}(s)$

  2. (f)

$\delta(S,w_{[0..i-1)})=T^{\prime}$ and $\delta(\langle
T^{\prime},s\rangle,\sigma)=\langle T,t\rangle$

  3. (g)

$w_{[i-1..]}\models\sigma\land{\mathbf{X}}\tau$

We are going to use the induction hypothesis to show that $w$ satisfies the
disjunct corresponding to $\langle\sigma,T^{\prime}\rangle$. The first
conjunct is satisfied from (f,g) and (I.H.1). From (d) it follows that for
every $j\in[0..i)$ the tuple $\langle w[j],\delta(S,w_{[0..j)})\rangle$ is not
in $\mathsf{Leave}(s)$. Thus for every
$\langle\eta,L\rangle\in\mathsf{Leave}(s)$, we either have
$w_{[j..]}\not\models\eta$ or $\delta(S,w_{[0..j)})\neq L$. Thus by (I.H.1)
and (f,g) we obtain that $w$ satisfies the second conjunct. Analogously, from
(c) it follows that for every $j\in[1..i)$ and for every
$\langle\rho,B^{\prime}\rangle\in\mathsf{Stay}(s)$ such that $\delta(\langle
B^{\prime},s\rangle,\rho)=\langle B,b\rangle$, either
$\delta(S,w_{[0..j-1)})\neq B^{\prime}$ or
$w_{[j-1..]}\not\models\rho\land{\mathbf{X}}\beta$. Thus by (I.H.1) and (f,g)
we obtain that $w$ satisfies the third and final conjunct.

Reachability formula 4

We want to prove the following equivalence:

$\begin{array}[]{cl}&w\models\langle S,s\rangle\xrightarrow[\bcancel{\langle
B,b\rangle\left(\beta\right)}]{\text{\tiny weak}}\langle
T,t\rangle\left(\tau\right)\\\\[18.00005pt] \iff&\forall i\geq
0.\leavevmode\nobreak\ \big{(}(\delta(\langle S,s\rangle,w_{[0..i)})=\langle
B,b\rangle\land w_{[i..]}\models\beta)\\\ &\phantom{\forall i\geq
0.\leavevmode\nobreak\ }\qquad\lor(i>0\wedge\langle
w[i{-}1],\delta(S,w_{[0..i{-}1)})\rangle\in\mathsf{Leave}(s))\big{)}\\\
&\phantom{\forall i\geq 0.\leavevmode\nobreak\
}\rightarrow\leavevmode\nobreak\ (\exists j\in[0..i).\leavevmode\nobreak\
\delta(\langle S,s\rangle,w_{[0..j)})=\langle T,t\rangle\land
w_{[j..]}\models\tau)\end{array}$

($\Rightarrow$): Assume that $w$ satisfies the left-hand side of the
equivalence. Then we immediately obtain from the definition that either
$\delta(\langle S,s\rangle,w_{[0..0)})\neq\langle B,b\rangle$ or
$w_{[0..]}\not\models\beta$. Further, notice that if $w$ does not satisfy
$\varphi\coloneqq\langle S,s\rangle\xrightarrow[\bcancel{\langle
B,b\rangle\left(\beta\right)}]{\text{\tiny weak},>0}\langle
T,t\rangle\left(\tau\right)$, then necessarily $\delta(\langle
S,s\rangle,w_{[0..0)})=\langle T,t\rangle$ and $w_{[0..]}\models\tau$, and
thus the right-hand side trivially holds for all $i$ by instantiating $j$ with
$0$.

Thus we can assume that $w$ satisfies $\varphi$ and using the fact that at
least one of $\delta(\langle S,s\rangle,w_{[0..0)})=\langle B,b\rangle$ and
$w_{[0..]}\models\beta$ does not hold, we only need to prove the right-hand
side for $i>0$.

Since we have $w\models\varphi$, then either $w$ satisfies the disjunct $\psi$
in line (2) or there exists a
$\langle\sigma,T^{\prime}\rangle\in\mathsf{Stay}(s)$ with $\delta(\langle
T^{\prime},s\rangle,\sigma)=\langle T,t\rangle$ such that the matching
disjunct $\chi$ in (1) is satisfied by $w$. We assume that the first case
holds, and defer the second case to later.

Note, that when applying the induction hypothesis (I.H.2) to each conjunct of
$\psi$, we can simplify the nested existential quantification to
${\mathbf{false}}$, since $w\not\models{\mathbf{false}}$. Thus we obtain for
all $i\geq 0$:

  1. (a)

For every $\langle\eta,L\rangle\in\mathsf{Leave}(s)$ at least one of the
following statements holds:

    1. (i)

$\delta(S,w_{[0..i)})\neq L$

    2. (ii)

$w[i]\neq\eta$

  2. (b)

For every $\langle\rho,B^{\prime}\rangle\in\mathsf{Stay}(s)$ such that
$\delta(\langle B^{\prime},s\rangle,\rho)=\langle B,b\rangle$ at least one of
the following statements holds:

    1. (i)

$\delta(S,w_{[0..i)})\neq B^{\prime}$

    2. (ii)

$w[i]\neq\rho$

    3. (iii)

$w_{[i+1..]}\not\models\beta$

Because $w$ and the sequence of generated configurations does not contain a
combined letter that leaves $s$ due to (a), we do have $\langle
w[i],\delta(S,w_{[0..i)})\rangle\notin\mathsf{Leave}(s)$ for all $i\geq 0$.
Thus $\langle w[i],\delta(S,w_{[0..i)})\rangle\in\mathsf{Stay}(s)$ for all
$i\geq 0$. Further, due to (b) we either do not see a combined letter at
position $i$ that enters the configuration $\langle B,b\rangle$ (and thus
$\delta(\langle S,s\rangle,w_{[i+1..]})=\langle B,b\rangle$) or the infinite
suffix of $w_{[i+1..]}$ does not satisfy $\beta$. From this, we can conclude
that the right-hand side holds. (The case for $i=0$ was already established in
the second paragraph.)

We now assume that there exists a tuple $\langle\sigma,T^{\prime}\rangle$ such
that $w$ satisfies the matching disjunct $\chi$ of line (1). Note that the
existence of $\langle\sigma,T^{\prime}\rangle$ immediately implies $s=t$.
Moreover, we can assume that $w$ does not satisfy the disjunct $\psi$ from
line (2). Thus by applying (I.H.2), we know that there exists an $k\geq 0$
such that either $\delta(S,w_{[0..k)})=L$ and $w[k]=\eta$ from
$\langle\eta,L\rangle\in\mathsf{Leave}(s)$ or $\delta(S,w_{[0..k)})=B$,
$w[k]=\rho$, and $w_{[k+1..]}\models\beta$ for some
$\langle\rho,B^{\prime}\rangle\in\mathsf{Stay}(s)$ and $\delta(\langle
B^{\prime},s\rangle,\rho)=\langle B,b\rangle$. Thus when we apply the (I.H.2)
to the corresponding reachability formula of $\chi$ we obtain a
$k^{\prime}\in[0..k)$ such that $\delta(S,w_{[0..k^{\prime})})=T^{\prime}$ and
$w_{[k^{\prime}..]}\models\sigma\land{\mathbf{X}}\tau$. Observe that $\chi$ is
a conjunction of formulas with the shape

$S\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\cdot(\cdot)}$}}^{\hbox{\set@color$\scriptstyle\,\text{\tiny
weak}$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\cdot(\cdot)}$}}^{\hbox{\set@color$\scriptstyle\,\text{\tiny
weak}$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\cdot(\cdot)}$}}^{\hbox{\set@color$\scriptstyle\,\text{\tiny
weak}$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\cdot(\cdot)}$}}^{\hbox{\set@color$\scriptstyle\,\text{\tiny
weak}$}}}\mathrel{\mathchar 0\relax\symAMSa
04B}\\!\\!\scriptscriptstyle{}}}T^{\prime}\left(\sigma\land{\mathbf{X}}\tau\right)$

and we now apply the induction hypothesis to all reachability formulas. Since
they all share the same “target”, we can instantiate the nested existential
quantification to the same $j^{\prime}$ (where $j^{\prime}$ is the smallest
non-negative integer satisfying the condition) such that:

  1. (a)

$\delta(S,w_{[0..j^{\prime})})=T^{\prime}$

  2. (b)

$w[j^{\prime}]=\sigma$

  3. (c)

$w_{[j^{\prime}+1..]}\models\tau$

  4. (d)

For every $\langle\eta,L\rangle\in\mathsf{Leave}(s)$ and every
$i^{\prime}\in[0..j^{\prime}]$ at least one of the following statements holds:

    1. (i)

$\delta(S,w_{[0..i^{\prime})})\neq L$

    2. (ii)

$w[i^{\prime}]\neq\eta$

  5. (e)

For every $\langle\rho,B^{\prime}\rangle\in\mathsf{Stay}(s)$ such that
$\delta(\langle B^{\prime},s\rangle,\rho)=\langle B,b\rangle$ and every
$i^{\prime}\in[0..j^{\prime}]$ at least one of the following statements holds:

    1. (i)

$\delta(S,w_{[0..i^{\prime})})\neq B^{\prime}$

    2. (ii)

$w[i^{\prime}]\neq\rho$

    3. (iii)

$w_{[i^{\prime}+1..]}\not\models\beta$

In order to show that $w$ satisfy the right-hand side of the equation, let now
$i\geq 0$ be an arbitrary integer and we need to prove:

$\begin{array}[]{c}\big{(}(\delta(\langle S,s\rangle,w_{[0..i)})=\langle
B,b\rangle\land w_{[i..]}\models\beta)\lor(i>0\land\langle
w[i{-}1],\delta(S,w_{[0..i)})\rangle\in\mathsf{Leave}(s))\big{)}\\\
\rightarrow(\exists j\in[0..i).\leavevmode\nobreak\ \delta(\langle
S,s\rangle,w_{[0..j)})=\langle T,t\rangle\land
w_{[j..]}\models\tau)\end{array}$

The case $i=0$ was already discussed in the second paragraph. Further, if
$i>j^{\prime}+1$, then (a-c) show that $j$ can be instantiated with
$j^{\prime}+1$. Thus assume that $i\in[1..(j^{\prime}+1)]$. Further, since
$j^{\prime}$ was chosen to be the smallest integer such that (a-c) holds, we
can simplify the expression we need to prove to:

$(\delta(\langle S,s\rangle,w_{[0..i)})\neq\langle B,b\rangle\lor
w_{[i..]}\not\models\beta)\land\langle
w[i{-}1],\delta(S,w_{[0..i{-}1)})\rangle\in\mathsf{Stay}(s))$

Note that second conjunct is direct consequence of (d). For the first
conjunct, we proceed by contradiction and assume that $i$ is the smallest
integer such that:

$\delta(\langle S,s\rangle,w_{[0..i)})=\langle B,b\rangle\land
w_{[i..]}\models\beta$

Due to the already established second conjunct, we have $\langle
w[i-1],\delta(S,w_{[0..i-1)}\rangle)=\langle\rho,B^{\prime}\rangle\in\mathsf{Stay}(s)$
and $\delta(\langle B^{\prime},s\rangle,\rho)=\langle B,b\rangle$. But since
$i-1\in[0..j^{\prime}]$, we have a contradiction to (e).

($\Leftarrow$): We assume that $w$ satisfies the right-hand side. We first
consider the case that the nested existential quantification is not true for
any $i\geq 0$. Thus for all $i\geq 0$ it holds that:

  1. (a)

$\langle w[i],\delta(S,w_{[0..i)})\rangle\in\mathsf{Stay}(s)$

  2. (b)

$\delta(\langle S,s\rangle,w_{[0..i)})\neq\langle B,b\rangle$ or
$w_{[i..]}\not\models\beta$

Since $w$ satisfies the right-hand side, it is easy to see that we have either
$\langle S,s\rangle\neq\langle B,b\rangle$ or $w\not\models\beta$. Hence it
remains to show that $w\models\langle S,s\rangle\xrightarrow[\bcancel{\langle
B,b\rangle\left(\beta\right)}]{\text{\tiny weak},>0}\langle
T,t\rangle\left(\tau\right)$, which we do by showing that $w$ satisfies (2).
From (a,b) we obtain:

  1. (a’)

For every $\langle\eta,L\rangle\in\mathsf{Leave}(s)$ we have either
$\delta(S,w_{[0..i)})\neq L$ or $w[i]\neq\eta$.

  2. (b’)

Either $w_{[i+1..]}\not\models\beta$ or for every
$\langle\rho,B^{\prime}\rangle\in\mathsf{Stay}(s)$ such that $\delta(\langle
B^{\prime},s\rangle,\rho)=\langle B,b\rangle$ we have either
$\delta(S,w_{[0..i)})\neq B^{\prime}$ or $w[i]\neq\rho$.

We then apply the induction hypothesis (I.H.2) to (a’,b’) and obtain that $w$
satisfies the disjunct of line (2).

We now consider the second case and assume that there is a $j$ such that:

  1. (a)

$\delta(\langle S,s\rangle,w_{[0..j)})=\langle T,t\rangle$

  2. (b)

$w_{[j..]}\models\tau$

Without loss of generality, we can assume $j$ to be the smallest integer with
such a property. Further, since $w$ satisfies the right-hand side, we have:

  1. (c)

$\forall i\in[0..j).\leavevmode\nobreak\ \langle
w[i],\delta(S,w_{[0..i)})\rangle\in\mathsf{Stay}(s)$

  2. (d)

$\forall i\in[0..j].\leavevmode\nobreak\ \delta(\langle
S,s\rangle,w_{[0..i)})\neq\langle B,b\rangle\lor w_{[i..]}\not\models\beta$

If $j=0$, then $w$ immediately satisfies the left-hand side. Thus assume
$j>0$. Due to (c), we have that $\langle\sigma,T^{\prime}\rangle=\langle
w_{[j-1]},\delta(S,w_{[0..j-1)})\rangle\in\mathsf{Stay}(s)$ and
$\delta(\langle\delta(S,w_{[0..j-1)}),s\rangle,w_{[j-1]})=\langle T,t\rangle$.
Thus there exists a matching disjunct for $\langle\sigma,T^{\prime}\rangle$ in
line (1) and we know it is satisfied by $w$ due the $(a,b,d)$ and the
induction hypothesis (I.H.2).

Reachability formula 5

We want to prove the following equivalence:

$\begin{array}[]{cl}&w\models\langle
S,s\rangle\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\dabar@\dabar@\dabar@\dabar@}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle\left(\beta\right)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\dabar@\dabar@\dabar@\dabar@}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle\left(\beta\right)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\dabar@\dabar@\dabar@\dabar@}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle\left(\beta\right)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\dabar@\dabar@\dabar@\dabar@}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle\left(\beta\right)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa 04B}\\!\\!\scriptscriptstyle{}}}\langle
T,t\rangle\left(\tau\right)\\\\[18.00005pt] \iff&\exists i_{1},i_{2}\geq
0.\leavevmode\nobreak\ \delta(\langle S,s\rangle,w_{[0..i_{1})})=\langle
T,t\rangle\land w_{[i_{1}..]}\models\tau\\\ &\phantom{\exists i_{1},i_{2}\geq
0.\leavevmode\nobreak\ }\land\leavevmode\nobreak\ (\exists
j_{1}\in[0..i_{1}).\leavevmode\nobreak\ \langle
w[j_{1}],\delta(S,w_{[0..j_{1}))}\in\mathsf{Enter}(s)\rangle)\\\
&\phantom{\exists i_{1},i_{2}\geq 0.\leavevmode\nobreak\
}\land\leavevmode\nobreak\ \langle
w[i_{2}],\delta(S,w_{[0..i_{2})})\rangle\in\mathsf{Leave}(s)\\\
&\phantom{\exists i_{1},i_{2}\geq 0.\leavevmode\nobreak\
}\land\leavevmode\nobreak\ (\forall j_{2}\in[0..\max(i_{1}{-}1,i_{2})].\\\
&\qquad\qquad\qquad\qquad\delta(\langle S,s\rangle,w_{[0..j_{2})})\neq\langle
B,b\rangle\lor w_{[j_{2}..]}\not\models\beta)\end{array}$

($\Rightarrow$): We assume that

$w\models\langle
S,s\rangle\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\dabar@\dabar@\dabar@\dabar@}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle\left(\beta\right)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\dabar@\dabar@\dabar@\dabar@}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle\left(\beta\right)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\dabar@\dabar@\dabar@\dabar@}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle\left(\beta\right)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\dabar@\dabar@\dabar@\dabar@}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle\left(\beta\right)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa 04B}\\!\\!\scriptscriptstyle{}}}\langle
T,t\rangle\left(\tau\right)$

holds and proceed by first constructing a witness for $i_{2}$ and then one for
$i_{1}$.

($\exists i_{2}$): Since $w$ satisfies line (3), there must be a combined
letter $\langle\sigma,L\rangle\in\mathsf{Leave}(s)$ such that $w$ satisfies
the corresponding disjunct. We apply to this disjunct the induction hypothesis
(I.H.3) and instantiate the existential quantifier to $i_{2}$ (which we intend
to be the witness for $\exists i_{2}$) with the following properties:

  1. 1.

$\delta(\langle S,s\rangle,w_{[0..i_{2})})=\langle L,s\rangle$

  2. 2.

$w[i_{2}]=\sigma$ and $\delta(\langle S,s\rangle,w_{[0..i_{2})})\neq\langle
B,b\rangle\lor w_{[i_{2}..]}\not\models\beta$

  3. 3.

$\forall j_{2}\in[0..i_{2}).\leavevmode\nobreak\ \delta(\langle
S,s\rangle,w_{[0..j_{2})})\neq\langle B,b\rangle\lor
w_{[j_{2}..]}\not\models\beta$

  4. 4.

$\forall j_{2}\in[0..i_{2}).\leavevmode\nobreak\ \langle
w[j_{2}],\delta(S,w_{[0..j_{2})})\rangle\in\mathsf{Stay}(s)$.

Observe that due to (1,2) we have $\langle
w[i_{2}],\delta(S,w_{[0..i_{2})})\rangle\in\mathsf{Leave}(s)$ and together
with (2,3) one can see that $i_{2}$ is a sufficient witness for the $\exists
i_{2}$ in the right-hand side of the equation we want to prove. Note that
property (4) is not useless and will be of importance later.

($\exists i_{1}$): Since $w$ also satisfies lines (1,2), there must be a
combined letter $\langle\sigma,T^{\prime}\rangle\in\mathsf{Enter}(t)$ such
that $w$ satisfies the corresponding disjunct. We then apply the induction
hypothesis (I.H.1) to all terms of the matching conjunction in lines (1,2).
Since all reachability formulas share the same target configuration and
formula, we can instantiate all existential quantifiers to the same integer
$k$ by picking the smallest instance for each existential quantifier. Let now
$k$ be this smallest non-negative integer. We introduce the following two
abbreviations $T^{\prime\prime}=\delta(\langle
T^{\prime},\cdot\rangle,\sigma)$ and $R^{\prime}_{\eta}=\delta(\langle
R,\cdot\rangle,\eta)$ for some $\langle\eta,R\rangle\in\mathsf{Enter}(b)$.
Note that we can leave out the last state in the definition of
$T^{\prime\prime}$, since for all states $q,p$ the transition relation maps
the the same successor configuration, i.e., $\delta(\langle
T^{\prime},q\rangle,\sigma)=\delta(\langle T^{\prime},p\rangle,\sigma)$.
Analogously, for we omit it from $R^{\prime}_{\eta}$. We now list all relevant
properties of $k$ derived from applying the induction hypothesis:

  1. 5.

$\delta(S,w_{[0..k)})=T^{\prime}$

  2. 6.

$w[k]=\sigma$

  3. 7.

$w_{[k+1..]}\models T^{\prime\prime}\xrightarrow[\bcancel{\langle
B,b\rangle\left(\beta\right)}]{}\langle T,t\rangle\left(\tau\right)$

  4. 8.

For all $\langle\eta,R\rangle\in\mathsf{Enter}(b)$ and all $\ell\in[0..k)$ at
least one of the following statements is true:

    1. (a)

$\delta(S,w_{[0..\ell)})\neq R$

    2. (b)

$w[\ell]\neq\eta$

    3. (c)

$w_{[\ell+1..]}\not\models R^{\prime}_{\eta}\xrightarrow[\bcancel{\langle
T,t\rangle\left(\tau\right)}]{\text{\tiny weak}}\langle
B,b\rangle\left(\beta\right)$

We continue and apply the induction hypothesis to (7) and then obtain $i_{1}$
(which we intend to be the witness for $\exists i_{1}$) with the following
properties (already shifted to indices relative to $w$). Further, we can
assume $i_{1}$ to be the smallest integer with these properties.

  1. 9.

$\delta(T^{\prime\prime},w_{[k+1..i_{1})})=\langle T,t\rangle$ and
$w_{[i_{1}..]}\models\tau$

  2. 10.

$\forall j\in[(k+1)..i_{1}).\leavevmode\nobreak\
\delta(T^{\prime\prime},w_{[k+1..j)})\neq\langle B,b\rangle\lor
w_{[j..]}\not\models\beta$

  3. 11.

$\forall j\in[(k+1)..i_{1}).\leavevmode\nobreak\ \langle
w[j],\delta(\delta(T^{\prime},\sigma),w_{[k+1..j)})\rangle\in\mathsf{Stay}(t)$

From (5,6,9) we obtain that $\delta(\langle S,s\rangle,w_{[0..i_{1})})=\langle
T,t\rangle$ and that $w_{[i_{1}..]}\models\tau$ taking care of the first line
of the right-hand side of the equation. Further, by construction $\langle
w[k],\delta(S,w_{[0..k)})\rangle=\langle\sigma,T\rangle\in\mathsf{Enter}(t)$
and since $k<i_{1}$, we now know that the second line is satisfied by our
witness for $\exists i_{1}$. Next, we inline the definition of
$T^{\prime\prime}$ in (10) and obtain: $\forall
j\in[(k+1)..i_{1}).\leavevmode\nobreak\ \delta(\langle
S,s\rangle,w_{[0..j)})\neq\langle B,b\rangle\lor w_{[j..]}\not\models\beta$.
Thus in order to complete this direction of the proof it remains to show that:

$\forall j\in[(i_{2}+1)..k].\leavevmode\nobreak\ \delta(\langle
S,s\rangle,w_{[0..j)})\neq\langle B,b\rangle\lor w_{[j..]}\not\models\beta$

If $[(i_{2}+1)..k]$ is the empty set, we are done. Thus assume that $i_{2}<k$.
We proceed with a proof by contradiction and assume that there exists an index
$j\in[i_{2}+1..k]$ such that $\delta(\langle S,s\rangle,w_{[0..j)})=\langle
B,b\rangle$ and $w_{[j..]}\models\beta$. Due to (1) and (4), there must be
some $j^{\prime}\in[i_{2}..j{-}1]$ such that the combined letter
$\langle\eta,R\rangle=\langle
w[j^{\prime}],\delta(S,w_{[0..j^{\prime})})\rangle$ is in $\mathsf{Enter}(b)$.
Without loss of generality we can further assume that:

  1. 12.

$\forall j^{\prime\prime}\in[j^{\prime}..j).\leavevmode\nobreak\ \langle
w[j^{\prime\prime}],\delta(S,w_{[0..j^{\prime\prime})})\rangle\in\mathsf{Stay}(b)$

Note that $j^{\prime}<k$ and since (8a) and (8b) cannot be true we can
instantiate (8c) to:

$w_{[j^{\prime}+1..]}\not\models
R^{\prime}_{\eta}\xrightarrow[\bcancel{\langle
T,t\rangle\left(\tau\right)}]{\text{\tiny weak}}\langle
B,b\rangle\left(\beta\right)$

We now apply the induction hypothesis to this and obtain an index $\ell\geq
j^{\prime}+1$ such that the following two statements hold (already with
adjusted indices):

  1. 13.

At least one of the following statements hold:

    1. (a)

$\delta(\langle S,s\rangle,w_{[0..\ell)})=\langle T,t\rangle\wedge
w_{[\ell..]}\models\tau$

    2. (b)

$\ell>j^{\prime}+1\wedge\langle w[\ell-1],\delta(\langle
S,s\rangle,w_{[0..\ell-1)}\rangle\in\mathsf{Leave}(b)$

  2. 14.

$\forall j^{\prime\prime}\in[(j^{\prime}{+}1)..\ell).\leavevmode\nobreak\
\delta(\langle S,s\rangle,w_{[0..j^{\prime\prime})})\neq\langle B,b\rangle\lor
w_{[j^{\prime\prime}..]}\not\models\beta$

Since $j^{\prime}<j$ and since we assumed that $j$ is the smallest integer
satisfying $\delta(\langle S,s\rangle,w_{[0..j)})=\langle B,b\rangle$ and
$w_{[j^{\prime\prime}..]}\models\beta$, we can conclude with (14) that
$\ell\leq j$. However, we have a contradiction between (13a), $\ell\leq j\leq
k<i_{1}$, and $i_{1}$ being the smallest index reaching $\langle T,t\rangle$
and satisfying $\tau$. Thus (13b) must hold. However, since $\ell\leq j$ this
contradicts (12). Thus there cannot be such a $j$ and we can conclude this
direction.

($\Leftarrow$): Assume that $w$ satisfies the left-hand side. Then there
exists $i_{1},i_{2},j_{1}\geq 0$, further let $i_{1},i_{2}$ be the smallest
integers and let $j_{1}$ be the largest integer such that:

  1. (a)

$\delta(\langle S,s\rangle,w_{[0..i_{1})})=\langle T,t\rangle$

  2. (b)

$w_{[i_{1}..]}\models\tau$

  3. (c)

$j_{1}<i_{1}$

  4. (d)

$\langle w[j_{1}],\delta(S,w_{[0..j_{1})})\rangle\in\mathsf{Enter}(t)$

  5. (e)

$\langle w[i_{2}],\delta(S,w_{[0..i_{2})})\rangle\in\mathsf{Leave}(s)$

  6. (f)

$\forall j_{2}\in[0..\max(i_{1}-1,i_{2})].\leavevmode\nobreak\ \delta(\langle
S,s\rangle,w_{[0..j_{2})})\neq\langle B,b\rangle\lor
w_{[j_{2}..]}\not\models\beta$

Since $i_{2}$ is the smallest integer with this property, we have $\langle
w[k],\delta(S,w_{[0..k)})\rangle\in\mathsf{Stay}(s)$ for all
$k\in[0..i_{2}{-}1]$. Thus we can apply (I.H.3) to this and (e,f) to show that
$w$ satisfies line (3) for $\langle
w[i_{2}],\delta(S,w_{[0..i_{2})})\rangle=\langle\sigma,L\rangle\in\mathsf{Leave}(s)$.
In order to show the disjunct of (1) and (2), we need to identify a suitable
$\langle\sigma,T^{\prime}\rangle\in\mathsf{Enter}(t)$. We argue that
$\langle\sigma,T^{\prime}\rangle=\langle
w[j_{1}],\delta(S,w_{[0..j_{1})})\rangle$ is a suitable choice.

We proceed by first showing that $w$ satisfies line (1). Since $j_{1}$ is the
largest integer with such a property, we immediately get $\langle
w[k],\delta(S,w_{[0..k)})\rangle\in\mathsf{Stay}(s)$ for all
$k\in[j_{1}{+}1,i_{1}{-}1]$. By applying (I.H.3) we get:

$w_{[j_{1}+1..]}\models\delta(\langle
T^{\prime},\cdot\rangle,\sigma)\xrightarrow[\bcancel{\langle
B,b\rangle\left(\beta\right)}]{}\langle T,t\rangle\left(\tau\right)$

We now apply (I.H.1) and use (d) to establish that the first line is satisfied
by $w$. In order show that line (2) is satisfied it remains to show that for
all $k\in[0..j_{1}]$ and all $\langle\eta,L\rangle\in\mathsf{Enter}(b)$ either
$\delta(\langle S,s\rangle,w_{[0..k)})\neq\langle\eta,L\rangle$ or
$w_{[k..]}\not\models\eta\land{\mathbf{X}}\Big{(}\delta(\langle
R,\cdot\rangle,\eta)\xrightarrow[\bcancel{\langle
T,t\rangle\left(\tau\right)}]{\text{\tiny weak}}\langle
B,b\rangle\left(\beta\right)\Big{)}$.

We proceed by contradiction. Assume that there is $k\leq j_{1}$ such that
$\delta(\langle S,s\rangle,$ $w_{[0..k)})=\langle\eta,L\rangle$, $w[k]=\eta$,
and $w_{[k+1..]}\models\delta(\langle
R,\cdot\rangle,\eta)\xrightarrow[\bcancel{\langle
T,t\rangle\left(\tau\right)}]{\text{\tiny weak}}\langle
B,b\rangle\left(\beta\right))$. By applying (I.H.4) and adjusting the indices
we obtain:

$\begin{array}[]{rl}\forall i\geq k+1.&\big{(}(\delta(\langle
S,s\rangle,w_{[0..i)})=\langle T,t\rangle\land w_{[i..]}\models\tau)\\\
&\leavevmode\nobreak\ \leavevmode\nobreak\ \leavevmode\nobreak\
\lor\leavevmode\nobreak\ (i>k+1\land\langle
w[i{-}1],\delta(S,w_{[0..i{-}1)})\rangle\in\mathsf{Leave}(b))\big{)}\\\
&\rightarrow\leavevmode\nobreak\ (\exists j\in[k+1..i).\leavevmode\nobreak\
\delta(\langle S,s\rangle,w_{[0..j)})=\langle B,b\rangle\land
w_{[j..]}\models\beta)\end{array}$

By instantiating this with (a,b) we get:

$\exists j\in[k+1..i_{1}).\leavevmode\nobreak\ \delta(\langle
S,s\rangle,w_{[0..j)})=\langle B,b\rangle\land w_{[j..]}\models\beta$

However this contradicts (f).

Thus we can apply (I.H.1) to establish that $w$ satisfies (2). ∎

*

###### Proof.

Observe first that there is no circularity in the definitions of the five
reachability formulas, even though they are defined by each other: Formula 2
is defined on top of formula 1, which is defined on top of formulas 3 and 5,
while formulas 3, 4, and 5 are defined with respect to reachability formulas
over configurations of a lower level.

Let $i\geq 1$ be an arbitrary index. We prove the statement by induction on
the level $m$ of the configurations $S$, $B$, $T$ in the reachability
formulas. We split the proof to five cases corresponding to the five
reachability formulas.

Reachability formula 1. Let $\beta\in\Pi_{i}$ and let $\tau\in\Sigma_{i}$. We
proceed by an induction on the the configuration level $m$.

($m=0$): There is only one configuration of level $0$ and it is the empty
configuration. Thus $S=T=B=\langle\rangle$. Applying the definition we obtain:

$\langle\rangle\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle\rangle(\beta)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle\rangle(\beta)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle\rangle(\beta)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle\rangle(\beta)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptscriptstyle{}}}\langle\rangle\left(\tau\right)=(\neg\beta){\mathbf{U}}\tau$

Note that $\neg\beta\in\Sigma_{i}$ and thus the whole formula
$(\neg\beta){\mathbf{U}}\tau$ is also in $\Sigma_{i}$.

($m\rightarrow m+1$): Let $\langle S,s\rangle,\langle T,t\rangle,\langle
B,b\rangle\in Q_{1}\times\cdots\times Q_{m+1}$ be arbitrary configurations of
level $m+1$. Thus:

$\langle
S,s\rangle\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle(\beta)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle(\beta)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle(\beta)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt\resizebox{}{}{{\leavevmode\hbox{\hskip-0.89449pt\hbox{\set@color{$\thicksim$}}}}}\hskip
0.2pt}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle(\beta)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa 04B}\\!\\!\scriptscriptstyle{}}}\langle
T,t\rangle\left(\tau\right)=\langle S,s\rangle\xrightarrow[\bcancel{\langle
B,b\rangle\left(\beta\right)}]{}\langle T,t\rangle\left(\tau\right)\lor\langle
S,s\rangle\mathrel{\mathchoice{\mathrel{}\mathrel{\mathop{\dabar@\dabar@\dabar@\dabar@}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle\left(\beta\right)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\displaystyle{}}{\mathrel{}\mathrel{\mathop{\dabar@\dabar@\dabar@\dabar@}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle\left(\beta\right)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\textstyle{}}{\mathrel{}\mathrel{\mathop{\dabar@\dabar@\dabar@\dabar@}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle\left(\beta\right)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa
04B}\\!\\!\scriptstyle{}}{\mathrel{}\mathrel{\mathop{\dabar@\dabar@\dabar@\dabar@}\limits_{\hbox{\set@color$\scriptstyle\,\bcancel{\langle
B,b\rangle\left(\beta\right)}$}}^{\hbox{\set@color$\scriptstyle\,$}}}\mathrel{\mathchar
0\relax\symAMSa 04B}\\!\\!\scriptscriptstyle{}}}\langle
T,t\rangle\left(\tau\right)$