Introduction 1 and 2

1 files changed, 23 insertions, 2 deletions

diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex
index 8a274f5..a7a2eea 100644
--- a/Assignment1/assignment1.tex
+++ b/Assignment1/assignment1.tex
@@ -1,5 +1,8 @@
 \documentclass[a4paper]{scrartcl}
 
+\usepackage[backend=biber,natbib]{biblatex}
+\bibliography{library}
+
 \title{Model Checking}
 \subtitle{Assignment 1}
 \author{Camil Staps \and Erin van der Veen}
@@ -9,9 +12,22 @@
 \maketitle
 
 \section{Past Modalities in LTL}
-%TODO: Explain that past Modalities are not necessary for a complete logic
-%TODO: Explain that LTLP does make the logic more succinct (Paper 1)
+% Explain that past Modalities are not necessary for a complete logic
+% Explain that LTLP does make the logic more succinct (Paper 1)
 %TODO: Give example on what kind of things we want to express with LTLP
+This section of the book concerns an extension of LTL called ``Past Modalities''.
+The combination of LTL and Past Modalities is often called ``LTL-Past'' or LTLP,
+for the sake of brevity (and without compromising readability) we will use the first (LTL-Past) 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.
+It wasn't until later, after it was shown that past modalities do not increase the expressive power of LTL~\cite{Gabbay1980},
+that computing scientists stopped considering past modalities in favour of minimality.
+
+In 2003 Nicolas Markey showed that, while past modalities do not increase expressive power,
+they do make the LTL exponentially more succinct~\cite{Markey2003}.
+In particular, Markey shows that there is a class of LTL-Past formulas that are $O(n)$,
+but $\Omega(2^n)$ in LTL.
+Markey achieves this proof by providing an formula that is in exactly this class.
 
 \subsection{Syntax and Semantics}
 %TODO: Provide formal syntax
@@ -31,4 +47,9 @@
 \subsection{Minimal Bad Prefix in NuSMV}
 %TODO: Given a formula of the form vw^\omega, can we find a n \in \mathbb{N} such that vw^n is a bad prefix?
 
+\section{Contribution}
+%TODO: Like we are some immature group of children, we have to provide proof of contribution
+
+\printbibliography
+
 \end{document}