summaryrefslogtreecommitdiff
path: root/Assignment1/conversion.tex
diff options
context:
space:
mode:
authorErin van der Veen2018-04-13 20:57:10 +0200
committerErin van der Veen2018-04-13 20:57:10 +0200
commit61f0664a4fb1b0fe98569e7722527abd87b6c012 (patch)
tree5ccb904a12c2f998bbb2336ffdc61de6c9bb2f14 /Assignment1/conversion.tex
parentAdd an exercise about dual modalities (diff)
Introduction PLTL to LTL
Diffstat (limited to 'Assignment1/conversion.tex')
-rw-r--r--Assignment1/conversion.tex12
1 files changed, 12 insertions, 0 deletions
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