Efficient Normalization of Linear Temporal Logic

Formulas are put in negation normal form by “pushing negations” across all operators using the duality relations (e.g., \(\lnot (\varphi _1 \mathbin {\mathbf {U}}\varphi _2)\) is replaced by \(\lnot \varphi _1 \mathbin {\mathbf {R}}\lnot \varphi _2\)). These transformations only increase the size of the formula by one unit, and so the formula in negation normal form has size \(O(n)\). The formula \(\overline{\varphi }\) is defined inductively using the duality relations (e.g., \(\overline{\varphi _1 \mathbin {\mathbf {U}}\varphi _2} := \overline{\varphi _1} \mathbin {\mathbf {R}}\overline{\varphi _2}\), \(\overline{{\mathbf {X}}\varphi } := {\mathbf {X}}\overline{\varphi }\)); these transformations preserve the size of the formula. □

We proceed as follows:

By lemma 4.2(3), it suffices to show that they are equivalent under context \(\langle {C} \!\mid \! {B_{{\mathbf {G}}{\mathbf {F}}}} \rangle\) since \(B_{{\mathbf {G}}{\mathbf {F}}}\subseteq B\). We prove \(w \models {\mathbf {G}}\psi\) iff \(w \models \psi \mathbin {\mathbf {U}}{\mathbf {G}}\left({ {\psi }{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } }\right)\) iff \(w \models {\mathbf {G}}\left({ {\psi }{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } }\right)\mathbin {\mathbf {R}}\psi\) for every \(w \in L_{C | B_{{\mathbf {G}}{\mathbf {F}}}}\). So fix an arbitrary \(w \in L_{C | B_{{\mathbf {G}}{\mathbf {F}}}}\).

(\(\Rightarrow\)) Assume \(w \models {\mathbf {G}}\psi\). Then, in particular, we have \(w \models {\mathbf {F}}{\mathbf {G}}\psi\). By lemma 4.13, \((w_i \models \psi \Leftrightarrow { {\psi }{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } })\) holds for every i beyond the stabilization index of w with respect to C. So, in particular, we have \(w \models {\mathbf {F}}{\mathbf {G}}\left({ {\psi }{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } }\right)\). It follows that \(w \models {\mathbf {G}}\psi \wedge {\mathbf {F}}{\mathbf {G}}\left({ {\psi }{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } }\right),\) which, by the semantics of LTL, implies \(w \models \psi \mathbin {\mathbf {U}}{\mathbf {G}}\left({ {\psi }{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } }\right)\) and \(w \models {\mathbf {G}}\left({ {\psi }{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } }\right) \mathbin {\mathbf {R}}\psi\).

(\(\Leftarrow\)) Assume \(w \models \psi \mathbin {\mathbf {U}}{\mathbf {G}}\left({ {\psi }{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } }\right)\). By the semantics of LTL, there exists \(i \ge 0\) such that \(w_j \models \psi\) for every \(j \lt i\) and \(w_j \models { {\psi }{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } }\) for every \(j \ge i\). By lemma 4.13, since \(w \in L_{C | B_{{\mathbf {G}}{\mathbf {F}}}}\), we have \(w_j \models \psi\) for every \(j \ge i\). So \(w_j \models \psi\) holds for every \(j \ge 0\), and so \(w \models {\mathbf {G}}\psi\). For \({\mathbf {G}}\left({ {\psi }{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } }\right)\mathbin {\mathbf {R}}\psi \equiv {\mathbf {G}}\left({ {\psi }{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } }\right)\mathbin {\mathbf {M}}\psi \vee {\mathbf {G}}\psi\), either \({\mathbf {G}}\psi\) holds and we are already done or we can apply the previous argument with only \(j \le i\) instead of \(j \lt i\). □

We only prove the first case. If \(L_{C | B_{{\mathbf {G}}{\mathbf {F}}}} = \emptyset\), the proposition trivially holds. Let \(w \in L_{C | B_{{\mathbf {G}}{\mathbf {F}}}}\).

(\(\Rightarrow\)) Assume \(w \models \psi _1 \mathbin {\mathbf {W}}\psi _2\), and consider two cases. If \(w \models {\mathbf {G}}\psi _1\), then \(w \models \psi _1 \mathbin {\mathbf {U}}{\mathbf {G}}({ {\psi _1}{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } })\) (lemma 4.17), and so \(w \models \psi _1 \,\, \mathbin {\mathbf {U}}\,\, \left(\psi _2 \vee {\mathbf {G}}\left({ {\psi _1}{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } }\right)\right)\). If \(w \not\models {\mathbf {G}}\psi _1\), then we have \(w \models \psi _1 \mathbin {\mathbf {W}}\psi _2\) iff \(w \models \psi _1 \mathbin {\mathbf {U}}\psi _2\) by the semantics of LTL, and then \(w \models \psi _1 \mathbin {\mathbf {U}}\psi _2\) implies \(w \models \psi _1 \mathbin {\mathbf {U}}\left(\psi _2 \vee {\mathbf {G}}\left({ {\psi _1}{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } }\right)\right)\), also by the semantics of LTL.

(\(\Leftarrow\)) Assume \(w \models \psi _1 \mathbin {\mathbf {U}}\left(\psi _2 \vee {\mathbf {G}}\left({ {\psi _1}{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } }\right)\right)\). Then \(w \models \psi _1 \mathbin {\mathbf {U}}(\psi _2 \vee {\mathbf {G}}\psi _1)\) (Lemma 4.17, after distributing \(\mathbin {\mathbf {U}}\) over \(\vee\)), and since \(\psi _1 \mathbin {\mathbf {U}}(\psi _2 \vee {\mathbf {G}}\psi _1) \equiv \psi _1 \mathbin {\mathbf {W}}\psi _2,\) we are done. □

(1) The formula \({\varphi \langle C\rangle }\) belongs to \(\Sigma _2\). We show it by structural induction on \(\varphi\). The only non-trivial cases are \(\varphi = \varphi _1\mathbin {\mathbf {W}}\varphi _2\) and \(\varphi = \varphi _1\mathbin {\mathbf {R}}\varphi _2\). For either of the two cases, by the induction hypothesis, we have \({\varphi _k\langle C\rangle } \in \Sigma _2\) for \(k=1,2\). Further, since \({ {\varphi _k}{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } }\in \Pi _1\), we have \({\mathbf {G}}\left({ {\varphi _k}{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } }\right)\in \Pi _1\) as well. So \({\varphi _1\langle C\rangle } \mathbin {\mathbf {U}}\big ({\varphi _2\langle C\rangle } \vee {\mathbf {G}}\left({ {\varphi _1}{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } }\right)\big) \in \Sigma _2\) and \(\left({\varphi _1\langle C\rangle } \vee {\mathbf {G}}\big ({ {\varphi _2}{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } }\big)\right) \mathbin {\mathbf {M}}{\varphi _2\langle C\rangle } \in \Sigma _2\), and we are done.

(2) The formulas \(\varphi\) and \({\varphi \langle C\rangle }\) are equivalent under context \(\langle {C} \!\mid \! {B} \rangle\). By lemma 4.2(3), it suffices to show that \(\left(w \models \varphi \iff w \models {\varphi \langle C\rangle } \right)\) holds for every \(C \subseteq B_{{\mathbf {G}}{\mathbf {F}}}\) and for every \(w \in L_{C | B_{{\mathbf {G}}{\mathbf {F}}}}\). We proceed by structural induction on \(\varphi\). We use the identity \(\begin{align*} {\psi \langle C\rangle } = {\psi \langle C\cap B_{{\mathbf {G}}{\mathbf {F}}}\rangle }, \end{align*}\) which holds because the case distinctions in definition 4.10 only involve formulas \({\mathbf {G}}{\mathbf {F}}\chi\) such that \(\chi\) is a subformula of \(\psi\), and those formulas belong to \(B_{{\mathbf {G}}{\mathbf {F}}}\).

The base of the induction is \(\varphi \in \lbrace {\mathbf {t\hspace{-0.5pt}t}}, {\mathbf {ff}}, a, \lnot a\rbrace\). In all of these cases, we have \(\varphi = {\varphi \langle C\rangle }\) by definition, and we are done. All cases in which \({\varphi \langle C\rangle }\) is defined homomorphically are handled in the same way, and so we consider only the case \(\varphi = \psi _1 \mathbin {\mathbf {U}}\psi _2\). Fix \(C\subseteq B_{{\mathbf {G}}{\mathbf {F}}}\) and \(w \in L_{C | B_{{\mathbf {G}}{\mathbf {F}}}}\). We prove \(\left(w \models \varphi \iff w \models {\varphi \langle C\rangle } \right)\). Applying the induction hypothesis to \(\psi _1\) and \(\psi _2\), \(\psi _j\) and \({\psi _j\langle C\rangle }\) are equivalent under context \(\langle {C} \!\mid \! {B_{{\mathbf {G}}{\mathbf {F}}}} \rangle\). Moreover, \(w_i \in L_{C | B_{{\mathbf {G}}{\mathbf {F}}}}\) for all \(i \ge 0\) by the limit properties of \({\mathbf {G}}{\mathbf {F}}\)-subformulas, and this yields (2) \(\begin{align} \forall i. & (w_i \models \psi _j \iff w_i \models {\psi _j\langle C\rangle }) & \mbox{ for $j=1,2$.} \end{align}\) We get \(\begin{equation*} \begin{array}{lllll} w \models \psi _1 \mathbin {\mathbf {U}}\psi _2 & \iff & \exists k. ~ w_k \models \psi _2 \wedge (\forall \ell \lt k. ~ w_\ell \models \psi _1) & \mbox{(semantics of LTL)}\\ &\iff & \exists k. ~ w_k \models {\psi _2\langle C\rangle } \wedge (\forall \ell \lt k. ~ w_\ell \models {\psi _1\langle C\rangle }) & \mbox{(2)}\\ &\iff & w \models {\psi _1\langle C\rangle } \mathbin {\mathbf {U}}{\psi _2\langle C\rangle } & \mbox{(semantics of LTL)} \\ &\iff & w \models {(\psi _1 \mathbin {\mathbf {U}}\psi _2)\langle C\rangle } & \mbox{(definition of}\ {\langle \rangle }), \end{array} \end{equation*}\) which concludes the proof.

The remaining cases are \(\varphi = \psi _1 \mathbin {\mathbf {W}}\psi _2\) and \(\varphi = \psi _1 \mathbin {\mathbf {R}}\psi _2\). Fix \(C\subseteq B_{{\mathbf {G}}{\mathbf {F}}}\) and \(w \in L_{C | B_{{\mathbf {G}}{\mathbf {F}}}}\). By the induction hypothesis, (2) holds. We derive \(\begin{equation*} \begin{array}{rlll} w \models \psi _1 \mathbin {\mathbf {W}}\psi _2 &\iff & w \models \psi _1 \mathbin {\mathbf {U}}(\psi _2 \vee {\mathbf {G}}({ {\psi _1}{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } })) & \text{(Proposition 4.18)} \\ &\iff & w \models \,\, {\psi _1\langle C\rangle } \mathbin {\mathbf {U}}({\psi _2\langle C\rangle } \vee {\mathbf {G}}({ {\psi _1}{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } })) & \text{(2)} \\ &\iff & w \models \,\, {(\psi _1 \mathbin {\mathbf {W}}\psi _2)\langle C\rangle } & \mbox{(definition of}\ {\langle \rangle }). \end{array} \end{equation*}\) The case \(\varphi = \psi _1 \mathbin {\mathbf {R}}\psi _2\) is analogous.

(3) If \(C\subseteq C^{\prime },\) then \({\varphi \langle C\rangle } \models {\varphi \langle C^{\prime }\rangle }\). Follows from a straightforward structural induction, using \({ {\varphi }{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } } \models { {\varphi }{\langle \hspace{-2.13387pt}\langle {C^{\prime }}\rangle \hspace{-2.13387pt}\rangle } }\), and the monotonicity of all operators (recall that formulas are in negation normal form). □

By the Contextual Equivalence Lemma, we have \(\begin{equation*} \varphi \equiv \bigvee _{C\subseteq B} \left(\varphi \langle C \!\mid \! B \rangle \wedge \bigwedge _{\psi \in C} \psi \langle \hspace{-2.13387pt}\langle C \!\mid \! {\psi }\mathchoice{\!\!\downarrow }{\!\!\downarrow }{\downarrow }{\downarrow } \rangle \hspace{-2.13387pt}\rangle \right) \end{equation*}\) for any well-founded basis \((B, \prec)\), formulas \(\varphi \langle C \!\mid \! B \rangle\) satisfying conditions (i) and (ii), and formulas \(\psi \langle \hspace{-2.13387pt}\langle C \!\mid \! {\psi }\mathchoice{\!\!\downarrow }{\!\!\downarrow }{\downarrow }{\downarrow } \rangle \hspace{-2.13387pt}\rangle\) satisfying conditions (iii) and (iv) of the lemma.

We choose \((B, \prec)\) as in Definition 4.1. We have \(B = B_{{\mathbf {G}}{\mathbf {F}}}\uplus B_{{\mathbf {F}}{\mathbf {G}}}\). For every \(C\subseteq B\), we split \(C= M \uplus N\), where \(M := C\cap B_{{\mathbf {G}}{\mathbf {F}}}\) and \(N := C\cap B_{{\mathbf {F}}{\mathbf {G}}}\). For every \({\mathbf {F}}{\mathbf {G}}\psi \in N\) (recall that N only contains \({\mathbf {F}}{\mathbf {G}}\)-formulas) and \(C\subseteq {\psi }\mathchoice{\!\!\downarrow }{\!\!\downarrow }{\downarrow }{\downarrow }\), we define \(({\mathbf {F}}{\mathbf {G}}\psi)\langle \hspace{-2.13387pt}\langle C \!\mid \! {\psi }\mathchoice{\!\!\downarrow }{\!\!\downarrow }{\downarrow }{\downarrow } \rangle \hspace{-2.13387pt}\rangle := {\mathbf {F}}{\mathbf {G}}({ {\psi }{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } })\), and for every \({\mathbf {G}}{\mathbf {F}}\psi \in M\) and \(C\subseteq {\psi }\mathchoice{\!\!\downarrow }{\!\!\downarrow }{\downarrow }{\downarrow }\), we define \(({\mathbf {G}}{\mathbf {F}}\psi)\langle \hspace{-2.13387pt}\langle C \!\mid \! {\psi }\mathchoice{\!\!\downarrow }{\!\!\downarrow }{\downarrow }{\downarrow } \rangle \hspace{-2.13387pt}\rangle := {\mathbf {G}}{\mathbf {F}}({ {\psi }⟦ {N}⟧ })\), as in Definitions 4.10 and 4.15. By Propositions 4.14 and 4.16, \(\psi \langle \hspace{-2.13387pt}\langle C \!\mid \! {\psi }\mathchoice{\!\!\downarrow }{\!\!\downarrow }{\downarrow }{\downarrow } \rangle \hspace{-2.13387pt}\rangle\) satisfies conditions (iii) and (iv) of the Contextual Equivalence Lemma for every \(\psi \in B\) and \(C\subseteq {\psi }\mathchoice{\!\!\downarrow }{\!\!\downarrow }{\downarrow }{\downarrow }\). Finally, for every \(C\subseteq B,\) we define \(\varphi \langle C \!\mid \! B \rangle := {\varphi \langle C\rangle }\), as in definition 4.19. By proposition 4.21, \(\varphi \langle C \!\mid \! B \rangle\) satisfies conditions (i) and (ii) of the Contextual Equivalence Lemma. Applying the lemma, we obtain the following: \(\begin{align*} \varphi \equiv \bigvee _{C\subseteq B} \left(\varphi \langle C \!\mid \! B \rangle \wedge \bigwedge _{\psi \in C} \psi \langle \hspace{-2.13387pt}\langle C \!\mid \! {\psi }\mathchoice{\!\!\downarrow }{\!\!\downarrow }{\downarrow }{\downarrow } \rangle \hspace{-2.13387pt}\rangle \right)\,\, & \equiv \bigvee _{M \subseteq B_{{\mathbf {G}}{\mathbf {F}}}\\ N \subseteq B_{{\mathbf {F}}{\mathbf {G}}}} \left(\varphi \langle C \!\mid \! B \rangle \wedge \bigwedge _{\psi \in N} \psi \langle \hspace{-2.13387pt}\langle C \!\mid \! {\psi }\mathchoice{\!\!\downarrow }{\!\!\downarrow }{\downarrow }{\downarrow } \rangle \hspace{-2.13387pt}\rangle \wedge \bigwedge _{\psi \in M} \psi \langle \hspace{-2.13387pt}\langle C \!\mid \! {\psi }\mathchoice{\!\!\downarrow }{\!\!\downarrow }{\downarrow }{\downarrow } \rangle \hspace{-2.13387pt}\rangle \right) \\ & \equiv \bigvee _{M \subseteq B_{{\mathbf {G}}{\mathbf {F}}}\\ N \subseteq B_{{\mathbf {F}}{\mathbf {G}}}} \left({\varphi \langle M\rangle } \wedge \bigwedge _{{\mathbf {F}}{\mathbf {G}}\psi \in N} {\mathbf {F}}{\mathbf {G}}({ {\psi }{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } }) \wedge \bigwedge _{{\mathbf {G}}{\mathbf {F}}\psi \in M} {\mathbf {G}}{\mathbf {F}}({ {\psi }⟦ {N}⟧ })\right). \end{align*}\)

By Propositions 4.14, 4.16, and 4.21, the right-hand side is a Boolean combination of formulas of \(\Delta _2\), and so in \(\Delta _2\) itself. For the size, observe first that B contains at most n formulas, and so the right-hand side is a disjunction of at most \(2^{n}\) formulas. We bound the length of a disjunct. First we observe that \(|{\varphi \langle C\rangle }| \le O(n^2)\), which follows easily from Definition 4.19. (For the cases defined homomorphically, the proof is a direct application of the induction hypothesis; for the case \(\varphi = \psi _1 \mathbin {\mathbf {W}}\psi _2,\) we have \(|{\varphi \langle C\rangle }| \le |{\psi _1\langle C\rangle }| + |{\psi _2\langle C\rangle }| + |{ {\psi _2}{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } }| +2\), and the result follows from \(|{ {\psi _k}{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } }| \le n\); the case \(\varphi = \psi _1 \mathbin {\mathbf {R}}\psi _2\) is analogous.) From the definition of \({ {\varphi }{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } },\) we immediately obtain \(|{\mathbf {F}}{\mathbf {G}}\left({ {\varphi }{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } }\right)| \le n\), and, since for every formula \(\psi\) we have \(|\psi | = |\overline{\psi }|\), the same holds for \({\mathbf {F}}{\mathbf {G}}\left({ {\varphi }{\langle \hspace{-2.13387pt}\langle {C}\rangle \hspace{-2.13387pt}\rangle } }\right)\). So each disjunct has length at most \(O(n^2)+ n \cdot n \in O(n^2)\). So we obtain \(2^n \cdot O(n^2) \in 2^{O(n)}\) for the final bound. □

This follows from the following claims:

To prove (1), observe that \({\it sf}\,({ {\psi }{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } }) \subseteq \lbrace { {\psi ^{\prime }}{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } } \mid \psi ^{\prime } \in {\it sf}\,(\psi) \rbrace\). This can be proven by a straightforward induction, which is trivial for the cases where \({ {\psi }{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } }\) is defined homomorphically. For \(\psi = \psi _1 \mathbin {\mathbf {U}}\psi _2\), according to definition 4.10, either \({ {\psi }{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } } = {\mathbf {ff}}\) or \({ {\psi }{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } } = { {\psi _1}{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } } \mathbin {\mathbf {W}}{ {\psi _2}{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } }\). Since \({ {\psi }{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } }\) is in the right-hand set by definition with \(\psi ^{\prime } = \psi\), it remains to consider the subformulas of \({ {\psi _k}{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } }\) for \(k=1,2\). However, by the induction hypothesis, for any \(\psi ^{\prime \prime } \in {\it sf}\,({ {\psi _k}{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } }),\) there is a \(\psi ^{\prime } \in {\it sf}\,(\psi _k) \subseteq {\it sf}\,(\psi)\) such that \(\psi ^{\prime \prime } = { {\psi ^{\prime }}{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } }\), and we are done. Using the just proven inclusion, we have \(\begin{equation*} {\textstyle \bigcup } \lbrace {\it sf}\,({ {\psi }{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } }) : \psi \in {\it sf}\,(\varphi)\rbrace \subseteq \lbrace { {\psi ^{\prime }}{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } } : \psi ^{\prime } \in {\it sf}\,(\psi), \psi \in {\it sf}\,(\varphi) \rbrace = \lbrace { {\psi }{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } } : \psi \in {\it sf}\,(\varphi) \rbrace , \end{equation*}\) and the cardinality of the latter set is clearly no more than \(|{\it sf}\,(\varphi)|\). The case of \({ {\psi }⟦ {N}⟧ }\) follows by duality.

For (2), we prove the stronger claim \(|{\it sf}\,({\psi \langle M\rangle }) \cup {\it sf}\,({ {\psi }{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } })| \le 4 |{\it sf}\,(\psi)|\) by induction on \(\psi\). The base cases and those in which both \({\psi \langle M\rangle }\) and \({ {\psi }{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } }\) are defined homomorphically are straightforward. Let us show only the cases of \(\mathbin {\mathbf {U}}\) and \(\mathbin {\mathbf {W}}\), since \(\mathbin {\mathbf {M}}\) and \(\mathbin {\mathbf {R}}\) are completely analogous. For \(\psi = \psi _1 \mathbin {\mathbf {U}}\psi _2\), we have \({\psi \langle M\rangle } = {\psi _1\langle M\rangle } \mathbin {\mathbf {U}}{\psi _2\langle M\rangle }\) and either \({ {\psi }{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } } = {\mathbf {ff}}\) or \({ {\psi }{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } } = { {\psi _1}{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } } \mathbin {\mathbf {W}}{ {\psi _2}{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } }\). In the first case, by the induction hypothesis, \(|{\it sf}\,({\psi _k\langle M\rangle })| \le |{\it sf}\,({\psi _k\langle M\rangle }) \cup {\it sf}\,({ {\psi _k}{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } })| \le 4 |{\it sf}\,(\psi _k)|\) for \(k = 1,2\). The remaining subformulas in the left-hand side are only two, \({\mathbf {ff}}\) and \({\psi \langle M\rangle }\) itself, so they are at most \(4 |{\it sf}\,(\psi)|\). In the second case, \(\begin{equation*} {\it sf}\,({\psi \langle M\rangle }) \cup {\it sf}\,({ {\psi }{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } }) = ({\it sf}\,({\psi _1\langle M\rangle }) \cup {\it sf}\,({ {\psi _1}{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } })) \cup ({\it sf}\,({\psi _2\langle M\rangle }) \cup {\it sf}\,({ {\psi _2}{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } })) \cup \lbrace {\psi \langle M\rangle }, { {\psi }{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } }\rbrace , \end{equation*}\) so we have the bound \(4 |{\it sf}\,(\psi _1)| + 4 |{\it sf}\,(\psi _2)| + 2 \le 4 |{\it sf}\,(\psi)|\) by the induction hypothesis. For \(\psi = \psi _1 \mathbin {\mathbf {W}}\psi _2\), we have \({\psi \langle M\rangle } = {\psi _1\langle M\rangle } \mathbin {\mathbf {U}}({\psi _2\langle M\rangle } \vee {\mathbf {G}}({ {\psi _1}{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } }))\) and \({ {\psi }{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } } = { {\psi _1}{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } } \mathbin {\mathbf {W}}{ {\psi _2}{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } }\). The calculation above now holds after replacing the set \(\lbrace {\psi \langle M\rangle }, { {\psi }{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } }\rbrace\) at the end of the right-hand side by \(\lbrace {\psi \langle M\rangle }, { {\psi }{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } }, {\psi _2\langle M\rangle } \vee {\mathbf {G}}({ {\psi _1}{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } }), {\mathbf {G}}({ {\psi _1}{\langle \hspace{-2.13387pt}\langle {M}\rangle \hspace{-2.13387pt}\rangle } }) \rbrace\), so we obtain the bound \(4 |{\it sf}\,(\psi _1)| + 4 |{\it sf}\,(\psi _2)| + 4 \le 4 |{\it sf}\,(\psi)|\). □

For Equation (3), observe that, by the definition of the semantics of LTL, \(\varphi _1 \mathbin {\mathbf {W}}\varphi _2 \equiv \varphi _1 \mathbin {\mathbf {U}}\varphi _2 \vee {\mathbf {G}}\varphi _2\) holds for arbitrary formulas \(\varphi _1, \varphi _2\). For Equation (4), we proceed by invoking the Weak Contextual Equivalence Lemma (Lemma 4.3) with basis \(B = \lbrace \mathbf {G\hspace{-0.85355pt}F}\psi _2\rbrace\), main formula \(\varphi = \varphi _1[\psi _1 \mathbin {\mathbf {U}}\psi _2] \mathbin {\mathbf {W}}\varphi _2\), and contextual formulas \(\varphi \langle C \!\mid \! B \rangle = \varphi _1[\psi _1 \mathbin {\mathbf {W}}\psi _2] \mathbin {\mathbf {W}}\varphi _2\) for \(C = \lbrace \mathbf {G\hspace{-0.85355pt}F}\psi _2\rbrace\) and \(\varphi \langle C \!\mid \! B \rangle = \varphi _1[\psi _1 \mathbin {\mathbf {U}}\psi _2] \mathbin {\mathbf {U}}(\varphi _2 \vee ({\mathbf {G}}\varphi _1[{\mathbf {ff}}]))\) for \(C = \emptyset\). The conclusion of that lemma is exactly (4), but we have to prove its two premises.

First Premise: \(\varphi\) and \(\varphi \langle C \!\mid \! B \rangle\) are equivalent under context \(\langle {C} \!\mid \! {B} \rangle\).

For the case \(C = \lbrace \mathbf {G\hspace{-0.85355pt}F}\psi _2 \rbrace\), let \(w \models \mathbf {G\hspace{-0.85355pt}F}\psi _2\). We have to show \(\varphi _1[\psi _1 \mathbin {\mathbf {U}}\psi _2] \mathbin {\mathbf {W}}\varphi _2 \equiv ^w \varphi _1[\psi _1 \mathbin {\mathbf {W}}\psi _2] \mathbin {\mathbf {W}}\varphi _2\). By the semantics of LTL, we have \(\psi _1 \mathbin {\mathbf {U}}\psi _2 \equiv \psi _1 \mathbin {\mathbf {W}}\psi _2 \wedge {\mathbf {F}}\psi _2\); further, \(w \models \mathbf {G\hspace{-0.85355pt}F}\psi _2\) implies \({\mathbf {F}}\psi _2 \equiv ^w {\mathbf {t\hspace{-0.5pt}t}}\), and so we get \(\psi _1 \mathbin {\mathbf {U}}\psi _2 \equiv ^w \psi _1 \mathbin {\mathbf {W}}\psi _2\). Applying lemma 5.6(2), we obtain \(\varphi _1[\psi _1 \mathbin {\mathbf {U}}\psi _2] \mathbin {\mathbf {W}}\varphi _2 \equiv ^w \varphi _1[\psi _1 \mathbin {\mathbf {W}}\psi _2] \mathbin {\mathbf {W}}\varphi _2\), as desired.

For the case \(C = \emptyset\), let \(w \not\models \mathbf {G\hspace{-0.85355pt}F}\psi _2\). We have to show \(\varphi _1[\psi _1 \mathbin {\mathbf {U}}\psi _2] \mathbin {\mathbf {W}}\varphi _2 \equiv ^w \varphi _1[\psi _1 \mathbin {\mathbf {U}}\psi _2] \mathbin {\mathbf {U}}(\varphi _2 \vee ({\mathbf {G}}\varphi _1[{\mathbf {ff}}]))\). For \(⫤ ^w\), we prove the stronger \(⫤\): \(\begin{equation*} \begin{array}{lr} \varphi _1[\psi _1 \mathbin {\mathbf {U}}\psi _2] \mathbin {\mathbf {U}}(\varphi _2 \vee ({\mathbf {G}}\varphi _1[{\mathbf {ff}}])) \\ \hspace{20.0pt}\models \varphi _1[\psi _1 \mathbin {\mathbf {U}}\psi _2] \mathbin {\mathbf {U}}(\varphi _2 \vee ({\mathbf {G}}\varphi _1[\psi _1 \mathbin {\mathbf {U}}\psi _2]) &\text{(Lemma 5.6(1) and ${\mathbf {ff}}\models \psi _1 \mathbin {\mathbf {U}}\psi _2$)} \\ \hspace{20.0pt}\equiv \varphi _1[\psi _1 \mathbin {\mathbf {U}}\psi _2] \mathbin {\mathbf {W}}\varphi _2 &\text{(semantics of LTL).} \end{array} \end{equation*}\) For \(\models ^w\), assume \(w \models \varphi _1[\psi _1 \mathbin {\mathbf {U}}\psi _2] \mathbin {\mathbf {W}}\varphi _2\). We have to show \(w \models \varphi _1[\psi _1 \mathbin {\mathbf {U}}\psi _2] \mathbin {\mathbf {U}}(\varphi _2 \vee ({\mathbf {G}}\varphi _1[{\mathbf {ff}}]))\). Consider two cases:

Second Premise: The formula for context \(\emptyset\) entails the one for context \(\lbrace \mathbf {G\hspace{-0.85355pt}F}\psi _2 \rbrace\). \(\begin{equation*} \begin{array}{lr} \varphi _1[\psi _1 \mathbin {\mathbf {U}}\psi _2] \mathbin {\mathbf {U}}(\varphi _2 \vee ({\mathbf {G}}\varphi _1[{\mathbf {ff}}])) \\ \hspace{20.0pt}\models \varphi _1[\psi _1 \mathbin {\mathbf {W}}\psi _2] \mathbin {\mathbf {U}}(\varphi _2 \vee ({\mathbf {G}}\varphi _1[{\mathbf {ff}}])) &\text{(Lemma 5.6(1) and}\ \psi _1 \mathbin {\mathbf {U}}\psi _2 \models \psi _1 \mathbin {\mathbf {W}}\psi _2) \\ \hspace{20.0pt}\models \varphi _1[\psi _1 \mathbin {\mathbf {W}}\psi _2] \mathbin {\mathbf {U}}(\varphi _2 \vee ({\mathbf {G}}\varphi _1[\psi _1 \mathbin {\mathbf {W}}\psi _2])) &\text{(Lemma 5.6(1) and}\ {\mathbf {ff}}\models \psi _1 \mathbin {\mathbf {W}}\psi _2)\\ \hspace{20.0pt}\models \varphi _1[\psi _1 \mathbin {\mathbf {W}}\psi _2] \mathbin {\mathbf {W}}\varphi _2 & \text{(semantics of LTL)} \end{array} \end{equation*}\) □

We associate to each formula a rank, defined by \(\mathit {rank}({\varphi }) = |\varphi | + n_{u}({\varphi })\). Observe that a formula \(\varphi\) is in 1-form iff \(\mathit {rank}({\varphi }) = |\varphi |\). Throughout the proof, we say that a formula \(\varphi ^{\prime }\) satisfies the limit property if for every subformula \(\mathbf {G\hspace{-0.85355pt}F}\psi\) of \(\varphi ^{\prime }\) the formula \(\psi\) is a subformula of \(\varphi\) and every \(\mathbf {F\hspace{-0.85355pt}G}\)-subformula of \(\varphi ^{\prime }\) is also a subformula of \(\varphi\) (notice the asymmetry). Further, we say that a formula \(\varphi ^{\prime }\) satisfies the size property if \(|\varphi ^{\prime }| \le 4^{\mathit {rank}(\varphi)} \cdot |\varphi |\) from which the claimed size bound immediately follows.

We prove by induction on \(\mathit {rank}({\varphi })\) that \(\varphi\) is equivalent to a formula \(\varphi ^{\prime }\) in 1-form satisfying the limit and size properties. Within the inductive step, we proceed by a case distinction of \(\varphi\):

If \(\varphi = {\mathbf {t\hspace{-0.5pt}t}}, {\mathbf {ff}}, \mathbf {G\hspace{-0.85355pt}F}\psi , \mathbf {F\hspace{-0.85355pt}G}\psi\), then \(\varphi\) is already in 1-form and satisfies the limit and size properties.

If \(\varphi = \varphi _1 \wedge \varphi _2, \varphi _1 \vee \varphi _2, \varphi _1 \mathbin {\mathbf {U}}\varphi _2,\) then by the induction hypothesis \(\varphi _1\) and \(\varphi _2\) can be normalized into formulas \(\varphi _1^{\prime }\) and \(\varphi _2^{\prime }\) satisfying the limit and size properties. The formulas \(\varphi _1^{\prime } \wedge \varphi _2^{\prime }\), \(\varphi _1^{\prime } \vee \varphi _2^{\prime }\), \(\varphi _1^{\prime } \mathbin {\mathbf {U}}\varphi _2^{\prime }\) are then in 1-form (the latter because the additional \(\mathbin {\mathbf {U}}\)-node is above any \(\mathbin {\mathbf {W}}\)-node) and satisfy the limit property. The size property holds because \(\begin{equation*} \begin{array}{rlr} |\varphi _1^{\prime }| + |\varphi _2^{\prime }| + 1 & \le 4^{\mathit {rank}({\varphi _1})} \cdot |\varphi _1| + 4^{\mathit {rank}({\varphi _2})} \cdot |\varphi _2| + 1 & \!(\text{induction hypotheses}) \\ & \le 4^{\mathit {rank}({\varphi _1})+\mathit {rank}({\varphi _2})} \cdot (|\varphi _1| + |\varphi _2| + 1) \\ & \le 4^{\mathit {rank}({\varphi })} \cdot |\varphi | & \!(|\varphi _i| \le |\varphi | \text{ and } \sum _{i=1}^2 \mathit {rank}({\varphi _i}) \lt \mathit {rank}({\varphi })). \end{array} \end{equation*}\) If \(\varphi = {\mathbf {X}}\varphi _1\), then by the induction hypothesis there is a formula \(\varphi _1^{\prime }\) equivalent to \(\varphi _1\) in 1-form, and so \(\varphi\) is equivalent to \({\mathbf {X}}\varphi _1^{\prime }\), which is in 1-form and satisfies the limit and size properties.

If \(\varphi = \varphi _1 \mathbin {\mathbf {W}}\varphi _2\) and \(n_{u}({\varphi }) = 0\), then \(\varphi _1 \mathbin {\mathbf {W}}\varphi _2\) is already in 1-form and satisfies the limit and size properties.

If \(\varphi = \varphi _1 \mathbin {\mathbf {W}}\varphi _2\) and \(n_{u}({\varphi }) \gt 0\), then we proceed by a case distinction:

We prove that \(\varphi [\psi ] \equiv (\psi \wedge \varphi [{\mathbf {t\hspace{-0.5pt}t}}]) \vee \varphi [{\mathbf {ff}}]\) for every \(\psi\) such that \({\mathbf {G}}\psi \equiv \psi\)—that is, \(w \models \psi\) iff \(w_k \models \psi\) for all \(k \in \mathbb {N}\). This is a generalization of (5) and (6), since both \({\mathbf {G}}\hspace{1.0pt}\mathbf {G\hspace{-0.85355pt}F}\psi ^{\prime } \equiv \mathbf {G\hspace{-0.85355pt}F}\psi ^{\prime }\) and \({\mathbf {G}}\hspace{1.0pt}\mathbf {F\hspace{-0.85355pt}G}\psi ^{\prime } \equiv \mathbf {F\hspace{-0.85355pt}G}\psi ^{\prime }\) for any \(\psi ^{\prime }\). The new statement follows from the Weak Contextual Equivalence Lemma (Lemma 4.3) with basis \(\lbrace \psi \rbrace\) and formulas \(\varphi [\psi ]\langle \lbrace \psi \rbrace \rangle = \varphi [{\mathbf {t\hspace{-0.5pt}t}}]\) and \(\varphi [\psi ]\langle \emptyset \rangle = \varphi [{\mathbf {ff}}]\). It remains to prove that the premises of the lemma hold:

We proceed by induction on the number of proper limit subformulas of \(\varphi\). If \(\varphi\) does not contain any, then it is already in 1-2-form. Assume there exists such a proper limit subformula \(\psi\) that is smaller (or incomparable) to all other limit subformulas of \(\varphi\) according to the subformula order. We derive \(\varphi [ \quad ]\) from \(\varphi\) by replacing each limit-node labeled by \(\psi\) by the special atomic proposition \([ \quad ]\). We then apply lemma 5.9 to obtain \(\begin{equation*} \varphi [\psi ] \equiv (\psi \wedge \varphi [{\mathbf {t\hspace{-0.5pt}t}}]) \vee \varphi [{\mathbf {ff}}], \qquad \mbox{ where } \psi = \mathbf {G\hspace{-0.85355pt}F}\psi ^{\prime }, \mathbf {F\hspace{-0.85355pt}G}\psi ^{\prime } \ . \end{equation*}\) Note that \(\psi\) does not properly contain any limit subformula, and so it is in 1-2-form. Both \(\varphi [{\mathbf {t\hspace{-0.5pt}t}}]\) and \(\varphi [{\mathbf {ff}}]\) are still in 1-form, and they have one limit operator less than \(\varphi\). Thus, they can be normalized by the induction hypothesis into \(\varphi _1^{\prime }\) and \(\varphi _2^{\prime }\) in 1-2-form. Finally, \(\varphi ^{\prime } = (\psi \wedge \varphi _1^{\prime }) \vee \varphi _2^{\prime }\) is a Boolean combination of formulas in 1-2-form, so it is in 1-2-form. The number of nodes of \(T_{\varphi ^{\prime }}\) can be crudely bounded as follows: \(\begin{equation*} \begin{array}{rll} |\varphi ^{\prime }| & \le |\varphi _1^{\prime }| + |\varphi _2^{\prime }| + |\psi | + 2 \\ {[}1ex] & \le 3^{n_{\text{lim}}({\varphi [{\mathbf {t\hspace{-0.5pt}t}}]})} \cdot |\varphi [{\mathbf {t\hspace{-0.5pt}t}}]| + 3^{n_{\text{lim}}({\varphi [{\mathbf {ff}}]})} \cdot |\varphi [{\mathbf {ff}}]| + |\psi | + 2 & (\text{induction hypotheses}) \\ {[}1ex] & \le 3^{n_{\text{lim}}({\varphi [{\mathbf {t\hspace{-0.5pt}t}}]})} \cdot 2 \cdot |\varphi [{\mathbf {t\hspace{-0.5pt}t}}]| + |\psi | + 2 & (|\varphi [{\mathbf {t\hspace{-0.5pt}t}}]| = |\varphi [{\mathbf {ff}}]|\text{, idem for } n_{\mathrm{lim}}) \\ {[}1ex] & \le 3^{n_{\text{lim}}({\varphi [{\mathbf {t\hspace{-0.5pt}t}}]})} \cdot \big (2 \cdot (|\varphi | - |\psi | + 1) + |\psi | + 2\big) & (n_{\text{lim}}({\varphi [{\mathbf {t\hspace{-0.5pt}t}}]}) \le n_{\text{lim}}({\varphi }) - 1) \\ {[}1ex] & \le 3^{n_{\text{lim}}({\varphi }) - 1} \cdot (2 |\varphi | - |\psi | + 4) \\ {[}1ex] & \le 3^{n_{\text{lim}}({\varphi }) - 1} \cdot (3 |\varphi |) = 3^{n_{\text{lim}}({\varphi })} \cdot |\varphi | & (|\psi |, |\varphi | \ge 2). \end{array} \end{equation*}\)

To show that the size of the limit subformulas does not increase, let b be a bound on the size of the \(\mathbf {G\hspace{-0.85355pt}F}\)-subformulas of \(\varphi\). We claim that the size of each \(\mathbf {G\hspace{-0.85355pt}F}\)-subformula of \(\varphi ^{\prime }\) is also bounded by b (the case of \(\mathbf {F\hspace{-0.85355pt}G}\psi\) is analogous). Indeed, the \(\mathbf {G\hspace{-0.85355pt}F}\)-subformulas of \(\varphi ^{\prime }\) are \(\psi\) (which is already in \(\varphi\)) and the \(\mathbf {G\hspace{-0.85355pt}F}\)-subformulas of \(\varphi _1^{\prime }\) and \(\varphi _2^{\prime }\). Since the \(\mathbf {G\hspace{-0.85355pt}F}\)-subformulas of \(\varphi [{\mathbf {t\hspace{-0.5pt}t}}]\) and \(\varphi [{\mathbf {ff}}]\) can only have decreased in size, by the induction hypothesis the number of nodes of any \(\mathbf {G\hspace{-0.85355pt}F}\)-subformula of \(\varphi _1^{\prime }\) and \(\varphi _2^{\prime }\) is bounded by b, and we are done. □

Notice that (7) and (8) are instances of the Weak Contextual Equivalence Lemma (Lemma 4.3) with bases \(\lbrace \mathbf {F\hspace{-0.85355pt}G}\psi _1\rbrace\) and \(\lbrace \mathbf {G\hspace{-0.85355pt}F}\psi _2\rbrace\), respectively. In the case of (7), the contextual formulas are \((\mathbf {G\hspace{-0.85355pt}F}\varphi [\psi _1 \mathbin {\mathbf {W}}\psi _2])\langle \lbrace \mathbf {F\hspace{-0.85355pt}G}\psi _1\rbrace \rangle = \mathbf {G\hspace{-0.85355pt}F}\varphi [{\mathbf {t\hspace{-0.5pt}t}}]\) and \((\mathbf {G\hspace{-0.85355pt}F}\varphi [\psi _1 \mathbin {\mathbf {W}}\psi _2])\langle \emptyset \rangle = \mathbf {G\hspace{-0.85355pt}F}\varphi [\psi _1 \mathbin {\mathbf {U}}\psi _2]\). The premises of the lemma are satisfied:

For (7), the formulas are \((\mathbf {F\hspace{-0.85355pt}G}\varphi [\psi _1 \mathbin {\mathbf {U}}\psi _2])\langle \lbrace \mathbf {G\hspace{-0.85355pt}F}\psi _2\rbrace \rangle = \mathbf {F\hspace{-0.85355pt}G}\varphi [\psi _1 \mathbin {\mathbf {W}}\psi _2]\) and \((\mathbf {F\hspace{-0.85355pt}G}\varphi [\psi _1 \mathbin {\mathbf {U}}\psi _2])\langle \emptyset \rangle = \mathbf {F\hspace{-0.85355pt}G}\varphi [{\mathbf {ff}}],\) and the premises of the lemma also hold:

A \(\mathbf {G\hspace{-0.85355pt}F}\)-obstacle of a formula is a \(\mathbin {\mathbf {W}}\)-node or a \(\mathbin {\mathbf {U}}\)-node under a \(\mathbin {\mathbf {W}}\)-node inside a \(\mathbf {G\hspace{-0.85355pt}F}\)-node. Similarly, an \(\mathbf {F\hspace{-0.85355pt}G}\)-obstacle is a \(\mathbin {\mathbf {U}}\)-node or a \(\mathbin {\mathbf {W}}\)-node under a \(\mathbin {\mathbf {U}}\)-node inside a \(\mathbf {F\hspace{-0.85355pt}G}\)-node. Finally, an obstacle is either a \(\mathbf {G\hspace{-0.85355pt}F}\)-obstacle or an \(\mathbf {F\hspace{-0.85355pt}G}\)-obstacle. We proceed by induction on the number of obstacles of \(\mathbf {G\hspace{-0.85355pt}F}\varphi\) or \(\mathbf {F\hspace{-0.85355pt}G}\varphi\). If they have no obstacles, then they are already in normal form (definition 5.3).

Assume \(\mathbf {G\hspace{-0.85355pt}F}\varphi\) has at least one obstacle. Then \(\varphi\) contains at least one maximal \(\mathbin {\mathbf {W}}\)-node \(\psi _1 \mathbin {\mathbf {W}}\psi _2\). We derive \(\mathbf {G\hspace{-0.85355pt}F}\varphi [ \quad ]\) from \(\mathbf {G\hspace{-0.85355pt}F}\varphi\) by replacing each \(\mathbin {\mathbf {W}}\)-node labeled by \(\psi _1 \mathbin {\mathbf {W}}\psi _2\) by the special atomic proposition \([ \quad ]\). By Equation (7), \(\mathbf {G\hspace{-0.85355pt}F}\varphi [\psi _1 \mathbin {\mathbf {W}}\psi _2]\) is equivalent to \(\begin{equation*} \mathbf {G\hspace{-0.85355pt}F}\varphi [\psi _1 \mathbin {\mathbf {U}}\psi _2] \vee (\mathbf {F\hspace{-0.85355pt}G}\psi _1 \wedge \mathbf {G\hspace{-0.85355pt}F}\varphi [{\mathbf {t\hspace{-0.5pt}t}}]). \end{equation*}\) We claim that each of \(\mathbf {G\hspace{-0.85355pt}F}\varphi [\psi _1 \mathbin {\mathbf {U}}\psi _2]\), \(\mathbf {G\hspace{-0.85355pt}F}\varphi [{\mathbf {t\hspace{-0.5pt}t}}]\), and \(\mathbf {F\hspace{-0.85355pt}G}\psi _1\) has fewer obstacles than \(\mathbf {G\hspace{-0.85355pt}F}\varphi [\psi _1 \mathbin {\mathbf {W}}\psi _2]\) and so can be normalized by the induction hypothesis. Indeed, \(\mathbf {G\hspace{-0.85355pt}F}\varphi [\psi _1 \mathbin {\mathbf {U}}\psi _2]\), and \(\mathbf {G\hspace{-0.85355pt}F}\varphi [{\mathbf {t\hspace{-0.5pt}t}}]\) have at least one \(\mathbin {\mathbf {W}}\)-node less than \(\varphi\), and the number of \(\mathbin {\mathbf {U}}\)-nodes under a \(\mathbin {\mathbf {W}}\)-node, due to the maximality of \(\psi _1 \mathbin {\mathbf {W}}\psi _2\), has not increased, and as a consequence it has fewer \(\mathbf {G\hspace{-0.85355pt}F}\)-obstacles (and by definition no \(\mathbf {F\hspace{-0.85355pt}G}\)-obstacles). For \(\mathbf {F\hspace{-0.85355pt}G}\psi _1\), observe first that every \(\mathbf {F\hspace{-0.85355pt}G}\)-obstacle of \(\mathbf {F\hspace{-0.85355pt}G}\psi _1\) is a \(\mathbf {G\hspace{-0.85355pt}F}\)-obstacle of \(\mathbf {G\hspace{-0.85355pt}F}\varphi [\psi _1 \mathbin {\mathbf {W}}\psi _2]\). Indeed, the obstacles of \(\mathbf {F\hspace{-0.85355pt}G}\psi _1\) are the \(\mathbin {\mathbf {U}}\)-nodes and the \(\mathbin {\mathbf {W}}\)-nodes under \(\mathbin {\mathbf {U}}\)-nodes; the former were \(\mathbin {\mathbf {U}}\)-nodes under \(\mathbin {\mathbf {W}}\)-nodes in \(\varphi\), and the latter were \(\mathbin {\mathbf {W}}\)-nodes of \(\varphi\), and so both \(\mathbf {G\hspace{-0.85355pt}F}\)-obstacles of \(\mathbf {G\hspace{-0.85355pt}F}\varphi\). Moreover, \(\psi _1 \mathbin {\mathbf {W}}\psi _2\) is a \(\mathbf {G\hspace{-0.85355pt}F}\)-obstacle of \(\varphi\), but not an \(\mathbf {F\hspace{-0.85355pt}G}\)-obstacle of \(\mathbf {F\hspace{-0.85355pt}G}\psi _1\). Hence, the number of obstacles has decreased.

Assume now that \(\mathbf {F\hspace{-0.85355pt}G}\varphi\) has at least one obstacle. Then \(\varphi\) contains at least one maximal \(\mathbin {\mathbf {U}}\)-node \(\psi _1 \mathbin {\mathbf {U}}\psi _2\). We derive \(\mathbf {F\hspace{-0.85355pt}G}\varphi [ \quad ]\) from \(\mathbf {F\hspace{-0.85355pt}G}\varphi\) by replacing each \(\mathbin {\mathbf {U}}\)-node labeled by \(\psi _1 \mathbin {\mathbf {U}}\psi _2\) by the special atomic proposition \([ \quad ]\). By Equation (8), \(\mathbf {F\hspace{-0.85355pt}G}\varphi [\psi _1 \mathbin {\mathbf {U}}\psi _2]\) is equivalent to \(\begin{equation*} (\mathbf {G\hspace{-0.85355pt}F}\psi _2 \wedge \mathbf {F\hspace{-0.85355pt}G}\varphi [\psi _1 \mathbin {\mathbf {W}}\psi _2]) \vee \mathbf {F\hspace{-0.85355pt}G}\varphi [{\mathbf {ff}}]. \end{equation*}\) Each of \(\mathbf {G\hspace{-0.85355pt}F}\psi _2\), \(\mathbf {F\hspace{-0.85355pt}G}\varphi [\psi _1 \mathbin {\mathbf {W}}\psi _2]\), and \(\mathbf {F\hspace{-0.85355pt}G}\varphi [{\mathbf {ff}}]\) has fewer obstacles as \(\mathbf {F\hspace{-0.85355pt}G}\varphi [\psi _1 \mathbin {\mathbf {U}}\psi _2]\) and can be normalized by the induction hypothesis. The proof is as above.

The size of the formula increases at most by a factor of 3 on each step, and the number of steps is bounded by the number of both \(\mathbin {\mathbf {W}}\)-nodes and \(\mathbin {\mathbf {U}}\)-nodes in \(\varphi\), which is bounded by the total number of nodes in \(\varphi\). So the formula has at most \(3^{|\varphi |} |\varphi |\) nodes. □

Any LTL formula \(\varphi\) can be transformed into an equivalent \(\varphi ^{\prime }\) in 1-form of size \(|\varphi ^{\prime }| \le 4^{2|\varphi |} \cdot |\varphi |\) by proposition 5.8. Moreover, \(n_{\text{lim}}({\varphi ^{\prime }}) \le 2 \cdot |\varphi |\), since every \(\mathbf {F\hspace{-0.85355pt}G}\)-subformula of \(\psi ^{\prime }\) and every argument \(\psi\) of a \(\mathbf {G\hspace{-0.85355pt}F}\)-subformula of \(\varphi ^{\prime }\) is a subformula of \(\varphi\). In addition, \(|\psi | \le |\varphi |\) for every \(\mathbf {G\hspace{-0.85355pt}F}\psi\) subformula of \(\varphi\).

According to proposition 5.10, for every formula \(\varphi ^{\prime }\) in 1-form, there is an equivalent formula \(\varphi ^{\prime \prime }\) in 1-2-form with (9) \(\begin{equation} |\varphi ^{\prime \prime }| \le 3^{n_{\text{lim}}({\varphi ^{\prime }})} \cdot |\varphi ^{\prime }| \le 3^{2 |\varphi |} \cdot (4^{2|\varphi |} \cdot |\varphi |) \le 3^{2|\varphi |} \cdot 4^{3|\varphi |} \end{equation}\) This formula is a Boolean combination of limit formulas with at most \(|\varphi |\) nodes, not containing any proper limit node, and other temporal formulas containing neither limit nodes nor \(\mathbin {\mathbf {U}}\)-nodes under \(\mathbin {\mathbf {W}}\)-nodes. The latter are in \(\Sigma _2,\) and proposition 5.12 deals with the former. Notice that every \(\mathbf {G\hspace{-0.85355pt}F}\psi\) and \(\mathbf {F\hspace{-0.85355pt}G}\psi\) subformula has at most \(|\varphi |\) nodes and thus can be normalized into a formula with at most \(3^{|\varphi |} |\varphi |\) nodes. The result \(\varphi ^{\prime \prime \prime }\) of replacing these limit subformulas by their normal forms within \(\varphi ^{\prime \prime }\) is a Boolean combination of normal forms, and so we are done. The number of nodes in the resulting formula \(\varphi ^{\prime \prime \prime }\) is at most \(\begin{align*} |\varphi ^{\prime \prime \prime }| \le & ~ |\varphi ^{\prime \prime }| + n_{\text{lim}}({\varphi ^{\prime \prime }}) \cdot 3^{|\varphi |} \cdot |\varphi | \\ \le & ~ |\varphi ^{\prime \prime }| \cdot 3^{|\varphi |} \cdot (|\varphi | + 1) & (n_{\text{lim}}({\varphi ^{\prime \prime }}) \le |\varphi ^{\prime \prime }|) \\ \le & ~ 4^{3|\varphi |} \cdot 3^{3|\varphi |} \cdot (|\varphi | + 1) & (\text{by (9)}) \\ \le & ~ 4^{3|\varphi |} \cdot 4^{(3 \log _4 3 + \frac{1}{2}) |\varphi |} \le 4^{6|\varphi |} & (|\varphi | + 1 \le 4^{|\varphi |/2}). \end{align*}\) □

Let us first show that \(\mathcal {A}_\varphi\) belongs to \(\text {A1W}[i]\). It follows immediately from the definition of \(\mathcal {A}_\varphi\) that for every two states \(\langle \psi ,\Gamma \rangle , \langle \psi ^{\prime },\Gamma ^{\prime }\rangle\) of \(\mathcal {A}_\varphi\), if \(\langle \psi ,\Gamma \rangle \overset{}{\longrightarrow } \langle \psi ^{\prime },\Gamma ^{\prime }\rangle\), then \(\Gamma ^{\prime } \subseteq \Gamma\). So in every path, there are at most \((i-1)\) alternations between \(\Sigma\) and \(\Pi\) classes. Since the states of \(\alpha\) are those annotated with \(\Pi\) classes, there are also at most \((i-1)\) alternations between \(\alpha\) and non-\(\alpha\) states in a path.

To show that \(\mathcal {A}_\varphi\) has at most 2n states, observe that for every formula \(\psi\) there are at most two smallest classes of the syntactic-future hierarchy containing \(\psi\). So \(\mathcal {A}_\varphi\) has at most two states for each proper subformula of \(\varphi\).

To prove that \(\mathcal {A}_\varphi\) recognizes \(\mathcal {L}(\varphi)\) one shows by induction on \(\psi\) that \(\mathcal {A}_\psi\) recognizes \(\mathcal {L}(\psi)\) from every marked formula \({\psi }_{\scriptscriptstyle \Gamma }\). The proof is completely analogous to the one given in the work of Vardi [48]. □

By Lemma 6.8, some \(\text {A1W}[2]\) with \(O(|{\it sf}\,(\varphi _{\!M,N})|)\) states recognizes \(\mathcal {L}(\varphi _{M,N})\). So it suffices to show that \(|{\it sf}\,(\varphi _{M,N}) | \in O(|{\it sf}\,(\varphi)|)\), but this is lemma 4.24. □

Due to lemma 6.15, the alternating automaton \(\mathcal {A}_{M,N}\) that recognizes \(\mathcal {L}(\varphi _{M,N})\) belongs to \(\text {A1W}[2]\) and has \(O(n)\) states. Applying the construction of Lemma 6.13, we obtain a DRW with \(2^{2^{O(n)}}\) states and a single Rabin pair. Using the union operation for DRWs, we obtain a DRW for \(\varphi\) with \((2^{2^{O(n)}})^{2^{O(n)}} = 2^{2^{O(n)}}\) states and \(2^n\) Rabin pairs. □