\subsubsection{PLTL to LTL}
\erin
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 LTL formulas to automata.
We will explain more about this algorithm once we get to it.

\paragraph{Syntactic Algorithm}

\paragraph{Automata-based Algorithm}

\cbend
%TODO: 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