\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{%
		Note that 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$.
	\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}

\erin
\begin{enumerate}[resume]
	\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)$.\cbend%
			\footnote{\cbcolor{red}\cbstart
				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.\cbend}
		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$):
	\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 hence forth, 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
	\item Muller automata can be converted to LTL formulae~\cites{Maler1990, Maler1994}
\end{enumerate}

Converting an LTL formula to a B\"uchi automata is discussed in Section 5.2 of this book.
Much of this algorithm is the same,
we must just 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 = (\mathcal{Q}, 2^{AP}, \delta, \mathcal{Q}_0,\mathcal{F})$ where:
\begin{itemize}
	\item $\mathcal{Q}$ is the set of all elementary formulae $B \subseteq closure(\phi)$
	\item $\mathcal{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 : \mathcal{Q} \times 2^{AP} \rightarrow 2^\mathcal{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 = (\mathcal{Q}, \Sigma, \delta, \mathcal{Q}_0,F)$ where
	\begin{description}
		\item[$\mathcal{Q}$] is a finite set of states
		\item[$\Sigma$] is an alphabet
		\item[$\delta: \mathcal{Q} \times \Sigma \rightarrow \mathcal{Q}$] is a transition function
		\item[$\mathcal{Q}_0 \subseteq \mathcal{Q}$] is a set of initial states
		\item[$\mathcal{F} \subseteq \mathcal{P}(\mathcal{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}$.
	\end{description}
\end{definition}

Converting a NBA to a Muller automaton was shown to be possible by R. McNaughton~\cite{McNaughton1966}
and is part of what is known as McNaughton's theorem.
\cbend

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