path: root/Assignment1/conversion.tex

\erin
\subsubsection{PLTL to LTL}
Above, we stated that past modalities do not increase the expressive power of LTL.
In this section we prove this statement by demonstrating two algorithms that can convert a arbitrary PLTL formulas to initially equivalent LTL formulas.
The first algorithm was first presented by \citet{Gabbay1989} in 1989 and is based on syntactic rewriting.
The second algorithm makes use of the translation of PLTL formulas to automata and automata to LTL formulas.
This algorithm is described in more detail below.

\paragraph{Syntactic Algorithm}
\label{pltl:to-ltl:syntactic}
The syntactic algorithm as proposed by Gabbay has its foundation in the following three facts:%
	\footnote{%
		Gabbay used a slightly different, \enquote{non-strict} definition for the $\Uop$ and $\Sop$ operators.
		\camil
		We then get $\sigma \vDash_i \phi_1 \Uop \phi_2 \Leftrightarrow \exists_{j > i}[\sigma \vDash_j \phi_2]$ and $\sigma \vDash_k \phi_1$ for all $i < k < j$ (rather than $i \le k < j$), and similarly for $\Sop$.
		Thus, our $\phi \Uop \psi$ is equivalent to Gabbay's $\psi \lor \phi \land \phi \Uop \psi$.
		Gabbay's $\phi \Uop \psi$ is equivalent to our $\Xop (\phi \Uop \psi)$.
		Also for the $\Sop$ operator is not hard to convert PLTL formulas with the semantics of \cref{def:pltl:semantics-words} to Gabbay's variant or vice versa.
		\erin
		For this paragraph we will use Gabbay's definitions.}
\begin{enumerate}
	\item Every PLTL formula can be written using no other temporal operators than $\Sop$ and $\Uop$ operators.
	\item Every formula $\phi$ containing only the $\Sop$ and $\Uop$ operators can be written as a boolean combination of $\wfff \cup \wffp \cup \wffn$.%
		\footnote{%
			This is known as the Separation Theorem.
			It was originally proven by \citet{Gabbay1980}.
			Folklore has it that when Hans Kamp, a philosopher working on temporal logics, heard of the result, he went out and bought Gabbay a cake (\url{https://cstheory.stackexchange.com/a/29452}, retrieved April 19, 2018).}
	\item The same formula without past modalities $\psi$, a boolean combination of $\wfff \cup \wffn$, is initially equivalent to $\phi$.
\end{enumerate}
When these facts are considered in sequence,
they result in an algorithm that, given a PLTL formula, produces an initially equivalent LTL formula.
We will now consider these facts in more detail.

Step 1 of the algorithm was proven by Kamp in is 1968 PhD thesis \citep{Kamp1968}.
It can also be shown by a set of rewrite rules, the approach taken by \citet{Gabbay1989}.
The correctness then follows from the formal semantics of the operators.
We only need to rewrite $\Xop$ and $\Xop^{-1}$.
Gabbay also gives rewrite rules for $\square$, $\lozenge$ and their PLTL counterparts, but since we have defined them as derived operators this is not necessary.
The next and previous operators can be rewritten as:
\[
	\begin{array}{ll}
		\Pop\phi &\rightarrow\enspace \bot \Sop \phi\\
		\Xop\phi &\rightarrow\enspace \bot \Uop \phi
	\end{array}
\]

Step 2 of the algorithm entails rewriting the formula containing only $\Uop$ and $\Sop$ to a form where there is no $\Sop$ in the scope of a $\Uop$, nor vice versa.
Gabbay proves that this can by done in Theorem 2.4 of his paper via a tedious case distinction.
The different cases are listed below.
For the proofs of the equivalences, we refer the reader to the appendix of \citet{Gabbay1989}.
\begin{enumerate}
	\item Suppose $E = q \Sop (a \wedge \alpha \Uop \beta)$, then $E \equiv E_1 \vee E_2 \vee E_3$ where:
		\begin{align*}
			E_1 &= q \Sop a \wedge \alpha \Sop a \wedge \alpha \wedge \alpha \Uop \beta\\
			E_2 &= \beta \wedge (\alpha \wedge q) \Sop a\\
			E_3 &= q \Sop (\beta \wedge q \wedge \alpha \Sop a \wedge q \Sop a)
		\end{align*}
\end{enumerate}

\camil
\begin{remark}[Intuition Behind the Elimination Rules]
	The intuition behind Gabbay's first elimination rule is as follows.
	If $q \Sop (a \land \alpha \Uop \beta)$, we know that at some point $t$, $a$ held, and that after $t$, $q$ held until the present moment.
	For the moment of fulfilment of $\alpha \Uop \beta$ we distinguish three cases:
	\begin{enumerate}
		\item
			$\alpha$ continuously held since $t$, presently holds, and continues to hold until at some point in the future $\beta$ holds.
		\item
			$\alpha$ has held since $t$ and at present $\beta$ holds.
		\item
			$\alpha$ has held since $t$ until some moment in the past at which $\beta$ held.
	\end{enumerate}
	These cases correspond to the elements of the disjunction $E_1$, $E_2$ and $E_3$, respectively.
	Note that case 2 and 3 are only different because of Gabbay's non-strict semantics.

	It is now easy to reconstruct the case where $\Sop$ and $\Uop$ are swapped, i.e. $E = q \Uop (a \land \alpha \Sop \beta)$.
	In this case, $q$ holds from the next moment until some moment $t$ at which $a$ will hold.
	For the moment of fulfilment of $\alpha \Sop \beta$ we distinguish three cases:
	\begin{enumerate}
		\item
			$\beta$ held at some moment in the future. $\alpha$ held continuously after that moment, including the present moment and up to $t$.
		\item
			$\beta$ currently holds and $\alpha$ continuously holds until $t$.
		\item
			At some point in the future (before $t$), $\beta$ will hold, after which $\alpha$ continuously holds until $t$.
	\end{enumerate}
	Thus we get $E \equiv E_1 \lor E_2 \lor E_3$ where:
	\begin{align*}
		E_1 &= q \Uop a \land \alpha \Uop a \land \alpha \land \alpha \Sop \beta\\
		E_2 &= \beta \land (q \land \alpha) \Uop a\\
		E_3 &= q \Uop (\beta \land q \land \alpha \Uop a \land q \Uop a)
	\end{align*}
	The reasoning behind the other elimination rules is similar and will not be discussed in detail.
\end{remark}
\cbend

\begin{enumerate}[resume]
	\erin
	\item Suppose $E = (q \lor \alpha\Uop\beta) \Sop a$, then $E \equiv E_1 \vee E_2 \vee E_3$ where:
		\begin{align*}
			E_1 &= \bot \Sop a\\
			E_2 &= (\beta \lor \alpha \land \alpha \Uop \beta) \land (\neg a \lor \neg c) \Sop a\\
			E_3 &= \neg(\beta \lor \alpha \land \alpha \Uop \beta) \land (\neg a \lor \neg c) \Sop a \land (\neg a \land \neg\beta) \Sop (\neg q \land \neg a)
		\end{align*}
		where $c = (\neg a \land \neg\beta) \Sop (\neg q \land \neg a) \land \neg\alpha \land \neg\beta$.

	\item Suppose $E = q \Sop (a \wedge \neg (\alpha \Uop \beta))$, then $E \equiv E_1 \vee E_2 \vee E_3$ where:
		\begin{align*}
			E_1 &= (q \wedge \neg \beta) \Sop a \wedge \neg \beta \wedge \neg (\alpha \Uop \beta)\\
			E_2 &= \neg \alpha \wedge \neg \beta \wedge (\neg \beta \wedge q) \Sop a\\
			E_3 &= q \Sop (\neg \alpha \wedge \neg \beta \wedge q \wedge (\neg \beta \wedge q) \Sop a)
		\end{align*}

	\item Suppose $E = (q \vee \neg (\alpha \Uop \beta)) \Sop a$,
		then $E \equiv \neg (\neg a \Sop (\neg q \wedge (\alpha \Uop \beta) \wedge \neg a)) \wedge \Fop^{-1} a$,
		which can be reduced via rule 1.

	\item Suppose $E = (q \vee \alpha \Uop \beta) \Sop (a \wedge \alpha \Uop \beta)$, then $E \equiv E_1 \lor E_2 \lor E_3$ where:
		\begin{align*}
			E_1 &= \alpha \Sop a \wedge (\beta \vee \alpha \wedge \alpha \Uop \beta)\\
			E_2 &= \beta \lor \alpha \land \alpha\Uop\beta \land \neg (\neg\alpha \land \neg\beta \land \neg\beta\Sop\neg q) \Sop (\beta \land \alpha \Sop a)\\
			E_3 &= \neg (\neg\alpha \land \neg\beta \land \neg\beta\Sop\neg q) \Sop (\beta \land \alpha \Sop a) \land (\beta \vee \alpha \wedge \alpha \Uop \beta) \land \neg (\neg\beta \Sop \neg q)
		\end{align*}
	
	\item Suppose $E = (q \vee \alpha \Uop \beta) \Sop (a \wedge \neg(\alpha \Uop \beta))$, then $E \equiv E_1 \vee E_2 \vee E_3$ where:
		\begin{align*}
			E_1 &= ((\neg \beta \wedge q) \Sop a) \wedge \neg \alpha \wedge \neg \beta\\
			E_2 &= [q \vee \alpha \Uop \beta] \Sop [\neg \alpha \wedge \neg \beta \wedge (q \vee \alpha \Uop \beta) \wedge (\neg \beta \wedge q) \Sop a]\\
			E_3 &= (q \wedge \neg \beta) \Sop a \wedge \neg \beta \wedge \neg (\alpha \Uop \beta)
		\end{align*}
		$E_2$ has a $\Uop$ in a $\Sop$, but can be further rewritten using elimination 5.

	\item Suppose $E = (q \vee \neg(\alpha \Uop \beta)) \Sop (a \wedge \alpha \Uop \beta)$, then $E \equiv E_1 \vee E_2$ where:
		\begin{align*}
			E_1 &= [q \vee \neg (\alpha \Uop \beta)] \Sop [\beta \wedge (q \vee \neg (\alpha \Uop \beta)) \wedge (\alpha \wedge q) \Sop a]\\
			E_2 &= (\alpha \wedge q) \Sop a \wedge \alpha \wedge \alpha \Uop \beta
		\end{align*}
		$E_1$ can be further reduced using eliminations 8 and 4.

	\item Suppose $E = (q \vee \neg (\alpha \Uop \beta)) \Sop (a \wedge \neg (\alpha \Uop \beta))$, then $E \equiv \neg (E_1 \vee E_2 \vee E_3)$ where:
		\begin{align*}
			E_1 &= \square^{-1} (\neg a \vee \alpha \Uop \beta)\\
			E_2 &= (\neg a \vee \alpha \Uop \beta) \Sop (\neg q \wedge \alpha \Uop \beta \wedge \neg a)\\
			E_3 &= (\neg a \vee \alpha \Uop \beta) \Sop (\neg q \wedge \alpha \Uop \beta)
		\end{align*}

		\camil
		Since $\sigma \vDash_i E_2$ entails $\sigma \vDash_i E_3$ for all $i\in\mathbb N$, we also have $E \equiv \neg(E_1 \lor E_3)$.%
			\footnote{%
				According to \citet[p.~439]{Gabbay1989}, $E_3$ is \enquote{subsumed by} $E_2$.
				Assuming the straightforward understanding of subsumption ($\phi$ subsumes $\psi$ if and only if $\textsl{Words}(\phi) \supseteq \textsl{Words}(\psi)$), this is incorrect and $E_2$ is subsumed by $E_3$ instead.}
		The term\erin\ $E_3$ (and $E_2$) can be further eliminated, in particular using elimination 5.
		\cbend
\end{enumerate}

\erin
Note that these rules can only be applied when a $\Uop$ is within the scope of a $\Sop$.
In order to move an $\Sop$ out of the scope of a $\Uop$, consider that $\Sop$ and $\Uop$ are symmetrical.
The above equivalences also hold when the path is reversed, so similar elimination rules exist for the case that $\Sop$ occurs within the scope of $\Uop$.

The final step of the algorithm entails removing the pure past formulas from the boolean combination.
After all, these formulas are meaningless for $\vDash_0$, since (using Gabbay's definitions) these formulas can only say things about exclusive past time.

\camil
\begin{example}[A property for an Authentication System]
	\label{ex:pltl-to-ltl:authentication}
	Consider again the property from \cref{ex:pltl:authentication-system}, repeated here with less verbose names:
	$\phi = \square (c \rightarrow \lnot f \Sop s)$.
	This can be rewritten to a form with only $\Uop$ and $\Sop$:
	\begin{align*}
		\square(c \rightarrow \lnot f \Sop s)
		&\equiv \lnot \lozenge \lnot (c \rightarrow \lnot f \Sop s)\\
		&\equiv \lnot (\top \Uop (\lnot (c \rightarrow \lnot f \Sop s)))\\
		&\equiv \lnot (\top \Uop (c \land \lnot (\lnot f \Sop s))).
	\end{align*}
	With Gabbay's $\Uop$ and $\Sop$, this becomes (first rewriting the $\Sop$, then the $\Uop$):%
		\footnote{We will informally use $\rightarrow$ for rewriting here, reserving $\equiv$ for true equivalence.}
	\begin{align*}
		\lnot (\top \Uop (c \land \lnot(\lnot f \Sop s)))
		&\rightarrow \lnot (\top \Uop (c \land \lnot(s \lor \lnot f \land \lnot f \Sop s)))\\
		&\equiv \lnot (\top \Uop (c \land \lnot s \land (f \lor \lnot (\lnot f \Sop s)))) \\
		&\equiv \lnot (\top \Uop (c \land \lnot s \land f) \lor \top \Uop (c \land \lnot s \land \lnot (\lnot f \Sop s))) \\
		&\rightarrow \lnot \big(
			[c \land \lnot s \land f]
			\lor [\top \Uop (c \land \lnot s \land f)]
			\\&\quad\qquad\lor [c \land \lnot s \land \lnot (\lnot f \Sop s)]
			\lor [\top \Uop (c \land \lnot s \land \lnot (\lnot f \Sop s))]\big)\\
		&\equiv \lnot \big(
			[c \land \lnot s \land (f \lor \lnot (\lnot \Sop s))]
			\lor [\top \Uop (c \land \lnot s \land f)]
			\\&\quad\qquad\lor [\top \Uop (c \land \lnot s \land \lnot (\lnot f \Sop s))]\big)\\
		&\equiv
			\lnot [c \land \lnot s \land (f \lor \lnot (\lnot f \Sop s))]
			\land \lnot [\top \Uop (c \land \lnot s \land f)]
			\\&\quad\qquad\land \lnot [\top \Uop (c \land \lnot s \land \lnot (\lnot f \Sop s))]\\
		&\equiv
			[\lnot c \lor s \lor (\lnot f \land \lnot f \Sop s)]
			\land \lnot [\top \Uop (c \land \lnot s \land f)]
			\\&\quad\qquad\land \lnot [\top \Uop (c \land \lnot s \land \lnot (\lnot f \Sop s))]\\
	\end{align*}
	Only the subterm $\top \Uop (c \land \lnot s \land \lnot (\lnot f \Sop s))$ needs to be rewritten in step 2.
	Rule 3 applies (with $\Sop$ and $\Uop$ swapped).
	This gives:
	\begin{align*}
		\top \Uop (c \land \lnot s \land \lnot (\lnot f \Sop s))
		&\equiv
		\lnot s \Uop (c \land \lnot s) \land \lnot s \land \lnot (\lnot f \Sop s)
			\\&\qquad \lor f \land \lnot s \land \lnot s \Uop (c \land \lnot s)
			\\&\qquad \lor \top \Uop (f \land \lnot s \land \lnot s \Uop (c \land \lnot s))
	\end{align*}
	And hence our original formula is initially equivalent to:
	\begin{alignat*}{3}
		\phi \equiv_0\enspace
		& &&[\lnot c \lor s \lor (\lnot f \land \lnot f \Sop s)]
		\land \lnot [\top \Uop (c \land \lnot s \land f)]\\
		& &&\quad\land \lnot
			\big[
				\lnot s \Uop (c \land \lnot s) \land \lnot s \land \lnot (\lnot f \Sop s)
				\\& &&\qquad\qquad \lor f \land \lnot s \land \lnot s \Uop (c \land \lnot s)
				\\& &&\qquad\qquad \lor \top \Uop (f \land \lnot s \land \lnot s \Uop (c \land \lnot s))
			\big]
	\end{alignat*}
	In step 3, we remove the pure past formulas from the boolean combination:
	\begin{alignat*}{3}
		\phi \equiv_0\enspace
		& &&[\lnot c \lor s \lor \lnot f]
		\land \lnot [\top \Uop (c \land \lnot s \land f)]
		\\& &&\quad\land \lnot [\lnot s \Uop (c \land \lnot s) \land \lnot s]
		\\& &&\quad\land \lnot [f \land \lnot s \land \lnot s \Uop (c \land \lnot s)]
		\\& &&\quad\land \lnot [\top \Uop (f \land \lnot s \land \lnot s \Uop (c \land \lnot s))]\\
		\equiv_0\enspace
		& &&[\lnot c \lor s \lor \lnot f]
		\land \lnot [\top \Uop (c \land \lnot s \land f)]
		\\& &&\quad\land [\lnot (\lnot s \Uop (c \land \lnot s)) \lor s]
		\\& &&\quad\land [\lnot f \lor s \lor \lnot (\lnot s \Uop (c \land \lnot s))]
		\\& &&\quad\land \lnot [\top \Uop (f \land \lnot s \land \lnot s \Uop (c \land \lnot s))]
	\end{alignat*}
	We can rewrite this back to our semantics of $\Uop$:%
	\footnote{The first two terms (the first line of the original formula) are collapsed into one term.
		This is because Gabbay's $\phi \land \lnot(\top \Uop \lnot\phi)$ is equivalent to our $\lnot (\top \Uop \lnot\phi)$ (and hence $\square\phi$).
		The same can be done for the last two terms (the last two lines of the original formula).
		The third term can be rewritten via $\Xop$:
		$\lnot (\lnot \phi \Uop \psi) \lor \phi
			\enspace\rightarrow\enspace \psi \lor \lnot\Xop (\lnot\psi \Uop \phi)
			\enspace\equiv\enspace \lnot(\lnot \psi \land \Xop (\lnot \psi \Uop \phi))
			\enspace\equiv\enspace \lnot(\lnot\psi \Uop \phi)$.}
	\begin{align*}
		\dots &\rightarrow\enspace
			\lnot [\top \Uop (c \land \lnot s \land f)]
			\enspace\land\enspace \lnot (\lnot s \Uop (c \land \lnot s))
			\enspace\land\enspace \lnot [\top \Uop (f \land \lnot s \Uop (c \land \lnot s))]\\
		&\equiv\enspace
			\square\lnot(c \land \lnot s \land f)
			\enspace\land\enspace \lnot (\lnot s \Uop (c \land \lnot s))
			\enspace\land\enspace \square\lnot(f \land \lnot s \Uop (c \land \lnot s))\\
		&\equiv\enspace
			\square\lnot(c \land \lnot s \land f)
			\enspace\land\enspace \lnot \psi
			\enspace\land\enspace \square\lnot(f \land \psi)
			\quad \text{where $\psi = \lnot s \Uop (c \land \lnot s)$}\\
		&\equiv\footnotemark\enspace
			\lnot \psi
			\enspace\land\enspace \square\lnot(f \land \psi)
	\end{align*}
	\footnotetext{Because $\square\lnot(f \land \psi) \equiv \square\lnot(c \land \lnot s \land f)$.}
	Consider again the semantics of $c$, $s$ and $f$:
	if $c$, a connection is established.
	$s$ indicates that authentication succeeded; $f$ that authentication failed.
	Thus, $\psi$ means that a connection will be established without authentication success.
	The two terms of the conjunction then mean:
	\begin{itemize}
		\item $\lnot\psi$.
			A connection cannot be established without prior authentication success.
		\item $\square\lnot(f \land \psi)$.
			After an authentication failure, a connection cannot be established without prior authentication success.
	\end{itemize}
	The resulting LTL formula is reasonably succinct, but is clear that the PLTL formula is easier to construct and understand.

	Note that we have not proven that no smaller LTL formula exists.
	For an example of such a proof, see \cref{ex:succinctness}.
\end{example}

\begin{example}[Protocol Dependencies]
	In \cref{ex:pltl:protocol-dependencies}, we considered the PLTL formula
	$\square \big(\psi \rightarrow
			\lozenge^{-1} (\phi_3 \land
				\lozenge^{-1} (\phi_2 \land
					\lozenge^{-1} \phi_1))\big)$.
	By the definitions of $\square$ and $\lozenge^{-1}$, it is equivalent to
	\[
		\lnot\big(
			\top \Uop (
				\psi \land \lnot (
					\top \Sop (
						\phi_3 \land \top \Sop (\phi_2 \land \top \Sop \phi_1)
		)))\big).
	\]
	No other temporal operators besides $\Uop$ and $\Sop$ are used, so to transform it to an initially equivalent LTL formula step 1 is not needed.

	Rewriting the formula to Gabbay's definitions and separating the pure past formulas in step 2 proceeds as in the previous example.
	The exact steps are not shown here for reasons of brevity.
\end{example}

\erin
\paragraph{Automata-based Algorithm}
The Automata-based Algorithm, which we will call the semantic algorithm henceforth, is based on the following translations:
\begin{enumerate}
	\item PLTL formulas can be converted to B\"uchi automata~\cite{Lichtenstein1985}
	\item B\"uchi automata can be converted to deterministic Muller automata~\citep{Safra1988}
	\item Muller automata can be converted to LTL formulae~\cites{Maler1990, Maler1994}
\end{enumerate}

Converting an LTL formula to a B\"uchi automaton is discussed in Section 5.2 of this book.
Much of this algorithm is the same,
we only need to modify some figures and definitions in order to be able to apply it on PLTL formulae.
The first Definition we must change is 5.35:
\begin{definition}[Elementary Sets of PLTL Formulas]
	$B \subseteq closure(\phi)$ is \emph{elementary} if it is consistent with respect to propositional logic, maximal, and locally consistent with respect to the until and since operators.
\end{definition}
Modifying the definition of elementary sets means we must also change Figure 5.20.
Particularly, we must extend it with the property in Figure~\ref{fig:log_consistent}.
\begin{figure}
	\centering
	\begin{mdframed}
		\begin{enumerate}
			\setcounter{enumi}{3}
		\item B is \emph{locally consistent} with respect to the since operator, i.e., for all $\phi_1 \Sop \phi_2 \in closure(\phi)$:
			\begin{itemize}
				\item $\phi_2 \in B \Rightarrow \phi_1 \Sop \phi_2 \in B$
				\item $\phi_1 \Sop \phi_2 \in B$ and $\phi_2 \not\in B \Rightarrow \phi_1 \in B$
			\end{itemize}
		\end{enumerate}
	\end{mdframed}
	\caption{Properties of elementary sets of formulae}
	\label{fig:log_consistent}
\end{figure}

Furthermore, we need to modify the generation of the B\"uchi automaton.

Let $\phi$ be an PLTL formua over $AP$.
Let $\mathcal{G}_\phi = (Q, 2^{AP}, \delta, Q_0,\mathcal{F})$ where:
\begin{itemize}
	\item $Q$ is the set of all elementary sets of formulae $B \subseteq closure(\phi)$
	\item $Q_0 = \{B \in Q \mid \phi \in B\}$
	\item $\mathcal{F} = \{F_{\phi_1 \Uop \phi_2} \mid \phi_1 \Uop \phi_2 \in closure(\phi)\} \cup \{F_{\phi_1 \Sop \phi_2} \mid \phi_1 \Sop \phi_2 \in closure(\phi)\}$ where
		\begin{align*}
			F_{\phi_1 \Uop \phi_2} &= \{B \in Q \mid \phi_1 \Uop \phi_2 \not\in B \text{ or } \phi_2 \in B\}\\
			F_{\phi_1 \Sop \phi_2} &= \{B \in Q \mid \phi_1 \Sop \phi_2 \not\in B \text{ or } \phi_2 \in B\}
		\end{align*}
\end{itemize}
The transition relation $\delta : Q \times 2^{AP} \rightarrow 2^Q$ is given by:
\begin{itemize}
	\item If $A \neq B \cap AP$, then $\delta(B,A) = \emptyset$
	\item If $A = B \cap AP$, then $\delta(B,A)$ is the set of all elementary sets of formulas $B'$ satisfying
		\begin{enumerate}
			\item for every $\Xop \psi \in closure(\phi): \Xop\psi \in B \Leftrightarrow \psi \in B'$
			\item for every $\Xop^{-1} \psi \in closure(\phi): \Xop^{-1}\psi \in B' \Leftrightarrow \psi \in B$
			\item for every $\phi_1 \Uop \phi_2 \in closure(\phi):$
				\[
					\phi_1 \Uop \phi_2 \in B \Leftrightarrow (\phi_2 \in B \vee (\phi_1 \in B \wedge \phi_1 \Uop \phi_2 \in B'))
				\]
			\item for every $\phi_1 \Sop \phi_2 \in closure(\phi):$
				\[
					\phi_1 \Sop \phi_2 \in B' \Leftrightarrow (\phi_2 \in B' \vee (\phi_1 \in B' \wedge \phi_1 \Sop \phi_2 \in B))
				\]
		\end{enumerate}
\end{itemize}

The next step in the conversion algorithm is converting the B\"uchi Automaton into a deterministic Muller Automaton.
Let us first define the Muller Automaton:
\begin{definition}[Deterministic Muller Automaton]
	A deterministic Muller automaton~\cite{McNaughton1966} is a tuple $A = (Q, \Sigma, \delta, Q_0,\mathcal F)$ where
	\begin{itemize}
		\item $Q$ is a finite set of states
		\item $\Sigma$ is an alphabet
		\item $\delta: Q \times \Sigma \rightarrow Q$ is a transition function
		\item $Q_0 \subseteq Q$ is a set of initial states
		\item $\mathcal{F} \subseteq \mathcal{P}(Q)$ is a set of sets of states that define the acceptance condition. $A$ accepts exactly those runs in which the set of infinitely often occurring states in an element of $\mathcal{F}$.
		\qedhere
	\end{itemize}
\end{definition}

Converting NBAs to Muller automata was shown to be possible by \citet{McNaughton1966}
and is part of what is known as McNaughton's theorem.
There are multiple ways to convert a NBA to a Muller Automaton.
In this book we will describe Safra's Determinization Algorithm~\citep{Safra1988}.

Safra's algorithm is an algorithm to determinize B\"uchi automata, based on subset construction.
This means that we consider sets of states in the original automaton, like we did for the determinization of NFAs described in section 4.1.
These sets of states we call \emph{macrostates}.
In this book, we will not describe the underlying theory of Safra's algorithm.
Instead, we will provide a simple description.
A more thorough discussion of the algorithm is given by \citet{Roggenbach2002}.
We will mostly follow this description, with slight modifications.

Let $B = (Q, \Sigma, q_0, \delta, F)$ be a NBA.
Safra's algorithm returns an automaton without acceptance criterion where the states are constructed as trees of $Q$.
Once this automaton is returned,
an acceptance criterion must be chosen.
Given that we want to construct a Muller Automaton,
we create a set of sets of states containing trees.
For the purpose of this book, Safra's algorithm will therefore be considered to return a Muller Automaton $A = (Q', \Sigma, q_0', \delta', F')$.

Choose $V := \{1, 2, \dots, 2\cdot|Q|\}$ for denoting nodes in Safra trees.%
	\footnote{Safra trees are defined by \citet{Roggenbach2002}.
		In short, they are ordered trees with macrostates as labels.}

\begin{enumerate}
	\item $q_0'$ is the Safra tree consisting of only the node 1 labelled with macrostate $\{q_0\}$.
	\item For every input $a$ and tree $T$ with set $N$ of nodes,
		the value of the transition function $\delta'(T,a)$ is computed as follows:
		\begin{enumerate}
			\item Remove all marks ``!'' in $T$
				%TODO: this mark is not mentioned anywhere else right now. Perhaps explain the intuition first.
			\item For every node $v$ with macrostate $M$ such that $M \cap F \neq \emptyset$, create a new node $v' \in (V\setminus N)$, such that $v'$ becomes the youngest son of $v$ and carries the macrostate $M \cap F$.
			\item Perform subset construction on every $v$.
			\item Perform horizontal merge on every node $v$.
			\item Remove all nodes with empty macrostates.
			\item Perform vertical merge on node $v$.
		\end{enumerate}
	\item Prune all unreachable states.
	\item Create $F'$ such that for every subset $S$ of $Q'$ it holds that for some $v \in V$:
		\[
			S \in F' \Leftrightarrow (\forall_{\text{Tree } t \in S} [v \text{ is in } t]) \wedge \exists_{\text{Tree } t \in S} [v \text{ is marked in } t]
		\]
\end{enumerate}

The last step of the algorithm is converting the Muller automaton to an LTL formula based on the decomposition of automata as described by \citet{Maler1994}.
The decomposition of finite automata was first described by \citet{Krohn1965} and is known as the Krohn-Rhodes theorem.
This theorem, in combination with the work of \citet{Meyer1969}, allows for the translation of Muller automaton to LTL.

\begin{definition}[Cascade Product~\cite{Maler2010}]
	Let $A = (Q, \Sigma, \delta)$ be an automaton, and let $B = (Q \times \Sigma, Q', \delta')$ be an automaton such that for all $q \in Q$ and $q' \in Q'$, either $\delta'(q',(q,\sigma))$ is defined for all $\sigma \in \Sigma$ or it is undefined for every $\sigma$.
	The cascade product $A \circ B$ is the automaton $C = (\Sigma, Q'', \delta'')$ where
	\[
		Q'' = \{(q, q') \mid \delta'(q',(q,\sigma)) \ne \bot\}
	\]
	and
	\[
		\delta''((q,q'),\sigma) = (\delta(q',\sigma),\delta'(q',(q,\sigma)))
		\qedhere
	\]
\end{definition}
\begin{theorem}[Krohn-Rhodes Theorem]
	For every automaton $A$ there exists a cascade $C = B_1 \circ B_2 \circ \dots \circ B_n$ such that:
	\begin{enumerate}
		\item Each $B_i$ is a permutation-reset automaton\footnote{\label{note:definition-omitted}Definition omitted for brevity.}
		\item There is a homomorphism\footnote{See \cref{note:definition-omitted}.} $\phi$ from $C$ to $A$
		\item Any permutation in some $B_i$ is homomorphic to a subgroup of the transformation semigroup of $A$
	\end{enumerate}
\end{theorem}

The cascade product can then be used to create star-free regular sets.
These sets can then be transformed into LTL formulae.
We will not discuss this transformation in detail since it lies beyond the scope of this book.

\cbend
%Provide the syntactic algorithm to convert PLTL to LTL
%Provide algorithm via automata to convert PLTL to LTL
%TODO: In both cases make use of examples from SSH Paper