Organise in different files

1 files changed, 25 insertions, 0 deletions

diff --git a/Assignment1/intro.tex b/Assignment1/intro.tex
new file mode 100644
index 0000000..0ccd0ca
--- /dev/null
+++ b/Assignment1/intro.tex
@@ -0,0 +1,25 @@
+\subsection{Past Modalities in LTL}
+% 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
+\erin
+As mentioned in Remark 5.16, LTL can be extended with \emph{past modalities}.
+This section discusses this extension.
+The combination of LTL and Past Modalities is often called \enquote{LTL-Past} or PLTL.
+For the sake of brevity we will use the second (PLTL) to denote this combination.
+When temporal logic was first introduced by Arthur N. Prior in his 1957 book~\cite{Prior1957},
+the logic consisted of both past and future modalities.
+Only later, when it was shown that past modalities do not increase the expressive power of LTL~\cite{Gabbay1980},
+computing scientists stopped considering past modalities for reasons of minimality.
+
+\erin
+In 2003, Nicolas Markey showed that while past modalities do not increase expressive power,
+they can make LTL formulas exponentially more succinct~\cite{Markey2003}.
+In other words, there is a class of PLTL formulae%
+	\footnote{In keeping with the style of the rest of the book, we alternate between \enquote{formulas} and \enquote{formulae} and wish the reader best of luck with this.}
+	for which the size of all equivalent LTL formulas is $\Omega\left(2^n\right)$.
+Markey achieves this proof by providing a formula that is in exactly this class.
+Besides being smaller, PLTL formulas can also be easier to write and understand, as examples below will demonstrate.
+They are also included in many model checking tools, such as NuSMV.
+For this reason, it is useful to discuss them here.
+\cbend