From 61f0664a4fb1b0fe98569e7722527abd87b6c012 Mon Sep 17 00:00:00 2001
From: Erin van der Veen
Date: Fri, 13 Apr 2018 20:57:10 +0200
Subject: Introduction PLTL to LTL

---
 Assignment1/conversion.tex | 12 ++++++++++++
 Assignment1/intro.tex      |  2 +-
 2 files changed, 13 insertions(+), 1 deletion(-)

(limited to 'Assignment1')

diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index a133fcf..9e71692 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -1,4 +1,16 @@
 \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
diff --git a/Assignment1/intro.tex b/Assignment1/intro.tex
index 0ccd0ca..0d359f3 100644
--- a/Assignment1/intro.tex
+++ b/Assignment1/intro.tex
@@ -1,4 +1,4 @@
-\subsection{Past Modalities in LTL}
+\subsection{Past Modalities in LTL}\label{sec:intro}
 % Explain that past Modalities are not necessary for a complete logic
 % Explain that PLTL does make the logic more succinct (Paper 1)
 %TODO: Give example on what kind of things we want to express with PLTL
-- 
cgit v1.2.3