\erin
\subsubsection{PLTL to LTL}
In Subsection~\ref{sec:intro} we stated that past modalities do not increase the expressive power of LTL.
In this section we proof this statement by demonstrating two algorithms that can convert any arbitrary PLTL formula to a LTL formula.
The first algorithm that we will demonstrate was first presented by Gabbay in 1989~\cite{Gabbay1989} and is based on syntactic rewriting.
The second algorithm makes use of the translation of PLTL formulas to automata and automata to LTL formulas.
We will explain more about this algorithm once we get to it.

\erin
\paragraph{Syntactic Algorithm}
The syntactic algorithm as proposed by Gabby has its foundation in the following three facts\footnote{Note that Gabbay used a slightly different definition for the $\Uop$ and $\Sop$ operators. For this paragraph of the book we will assume $\phi \Uop \psi := \Xop (\phi \Uop \psi)$ and $\phi \Sop \psi := \Xop^{-1} (\phi \Sop \psi)$. For a given formula, it is not hard to convert it to this form.}:
\begin{enumerate}
	\item Every PLTL formula can be written using only the $\Sop$ and $\Uop$ operators.
	\item Every formula containing only the $\Sop$ and $\Uop$ operators can be written in the following form: $F \cup P \cup A$ where $F$ are the future modalities ($\Uop$), $P$ are the past modalities ($\Sop$), and $A$ are the atomic expressions.
	\item When removing $P$ from this formula, the resulting formula is equivalent to the formula we started with when applied on position 0 in the path.
\end{enumerate}
When these facts are considered in sequence,
it is trivial to realise that it results in an algorithm that, given a PLTL formula, produces an initially equivalent LTL formula.
We will now show these facts in more detail.

Step 1 of the algorithm is trivially given using a rewrite system.
This rewrite system is given in Figure~\ref{fig:rewrite}.
\begin{figure}
	\centering
	\begin{alignat*}{2}
		&\Pop\phi       &&\leftrightarrow \bot \Sop \phi\\
		&\Xop\phi       &&\leftrightarrow \bot \Uop \phi\\
		&\Gop\phi       &&\leftrightarrow \neg (\top \Uop \neg \phi)\\
		&\Fop\phi       &&\leftrightarrow \top \Uop \phi\\
		&\Gop^{-1}\phi &&\leftrightarrow \neg (\top \Sop \neg \phi)\\
		&\Fop^{-1}\phi &&\leftrightarrow \top \Sop \neg
	\end{alignat*}
	\caption{The rewrite rules for writing any PLTL formula as a formula containing only $\Sop$ and $\Uop$.}
	\label{fig:rewrite}
\end{figure}
This full expressiveness of $\Uop$ and $\Sop$ is proven in the PhD. thesis of J. Kamp~\cite{Kamp1968},
and again by Gabbay using a different method~\cite{Gabbay1989}.

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$,
and there exists on $\Uop$ in the scope of a $\Sop$.
Gabby proofs that this can by done in Theorem 2.4 of his paper,
the rewrite rules are given in the Appendix of the same paper.
In this book, we will not proof that these rewrite rules hold, but they are given below.
\begin{enumerate}
	\item Suppose $E = q \Sop a \wedge (\alpha \Uop \beta))$ then it holds that $E = E_1 \vee E_2 \vee E_3$ if:
		\begin{align*}
			E_1 &= (q \Sop a) \wedge (\alpha \Sop a) \wedge \alpha (\alpha \Uop \beta)\\
			E_2 &= \beta \wedge (\alpha \Sop a) \wedge (q \Sop a)\\
			E_3 &= q \Sop \beta \wedge q \wedge (\alpha \Sop a) \wedge (q \Sop a)
		\end{align*}

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

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

	\item Suppose $E = q \vee \neg (\alpha \Uop \beta) \Sop a$ then it holds that $E = \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 it holds that $E = E_1 \vee (E_2 \wedge E_3)$ if:
		\begin{align*}
			E_1 &= (\alpha \Sop a) \wedge (\beta \vee (\alpha \wedge (\alpha \Uop \beta)))\\
			E_2 &= (\beta \vee \alpha \vee \neg(\neg\beta \Sop \neg q) \Sop \beta \wedge (\alpha \Sop a))\\
			E_3 &= (\beta \vee (\alpha \wedge (\alpha \Uop \beta))) \vee \neg (\neg\beta \Sop \neg q)
		\end{align*}
	
	\item Suppose $E = q \vee (\alpha \Uop \beta) \Sop a \wedge \neg(\alpha \Uop \beta)$ then it holds that $E = E_1 \vee E_2 \vee E_3$ if:
		\begin{align*}
			E_1 &= (\neg \beta \wedge q \Sop a) \wedge \neg \beta \wedge \neg \alpha\\
			E_2 &= q \vee (\alpha \Uop \beta) \Sop \neg \beta \wedge \neg \alpha \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*}

	\item Suppose $E = q \vee \neg(\alpha \Uop \beta) \Sop a \wedge (\alpha \Uop \beta)$ then it holds that $E = E_1 \vee E_2$ if:
		\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*}
		Where $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 it holds that $E = \neg \Gop^{-1}(E_1 \vee E_2 \vee E_3)$ if:
		\begin{align*}
			E_1 &= \neg a \vee \neg (\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*}
		After elimination of $\Gop^{-1}$, this formula can be further eliminated.
		In particular by using elimination 5.
\end{enumerate}
When considering these rules, it might be noted that they can only be applied when a $\Uop$ is within the scope of a $\Sop$.
In order to move the $\Sop$ out of the scope of the $\Uop$ we need to consider that these formulas also hold when the path is reversed.
I.e. we can also apply these eliminations when a $\Sop$ is within the scope of a $\Uop$.

The final step of the algorithm entails removing the part of the formula that contains the $\Sop$-operators.

\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}

\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