Step 1 of syntactic algorithm

1 files changed, 29 insertions, 2 deletions

diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 9e71692..e42d967 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -1,12 +1,39 @@
-\subsubsection{PLTL to LTL}
 \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 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.
 
+\erin
 \paragraph{Syntactic Algorithm}
+The syntactic algorithm as proposed by Gabby has its foundation in the following three facts:
+\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 \phi \Sop \bot\\
+		&\Xop\phi       &&\leftrightarrow \phi \Uop \bot\\
+		&\Gop\phi       &&\leftrightarrow \neg (\neg \phi \Uop \top)\\
+		&\Fop\phi       &&\leftrightarrow \phi \Uop \top\\
+		&\Gop^{--1}\phi &&\leftrightarrow \neg (\neg \phi \Sop \top)\\
+		&\Fop^{--1}\phi &&\leftrightarrow \phi \Sop \top
+	\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 theorem 2.3 of the paper by Gabbay~\cite{Gabbay1989}.
 
 \paragraph{Automata-based Algorithm}