Introduction 1 and 2

2 files changed, 86 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}
diff --git a/Assignment1/library.bib b/Assignment1/library.bib
new file mode 100755
index 0000000..d9f35e4
--- /dev/null
+++ b/Assignment1/library.bib
@@ -0,0 +1,63 @@
+@Article{Markey2003,
+  author    = {Markey, Nicolas},
+  title     = {Temporal logic with past is exponentially more succinct},
+  journal   = {EATCS Bulletin},
+  year      = {2003},
+  volume    = {79},
+  pages     = {122--128},
+  publisher = {European Association for Theoretical Computer Science},
+}
+
+@InProceedings{Gabbay1989,
+  author       = {Gabbay, Dov},
+  title        = {The declarative past and imperative future: executable temporal logic for interactive systems},
+  booktitle    = {Temporal logic in specification},
+  year         = {1989},
+  organization = {Springer},
+  pages        = {409--448},
+}
+
+@InProceedings{Lichtenstein1985,
+  author       = {Lichtenstein, Orna and Pnueli, Amir and Zuck, Lenore},
+  title        = {The glory of the past},
+  booktitle    = {Workshop on Logic of Programs},
+  year         = {1985},
+  organization = {Springer},
+  pages        = {196--218},
+}
+
+@InProceedings{Gabbay1980,
+  author       = {Gabbay, Dov and Pnueli, Amir and Shelah, Saharon and Stavi, Jonathan},
+  title        = {On the temporal analysis of fairness},
+  booktitle    = {Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
+  year         = {1980},
+  organization = {ACM},
+  pages        = {163--173},
+}
+
+@Article{Moser1994,
+  author    = {Moser, Louise E. and Melliar-Smith, PM and Kutty, George and Ramakrishna, YS},
+  title     = {Completeness and soundness of axiomatizations for temporal logics without next},
+  journal   = {Fundamenta Informaticae},
+  year      = {1994},
+  volume    = {21},
+  number    = {4},
+  pages     = {257--305},
+  publisher = {IOS Press},
+}
+
+@InProceedings{Laroussinie2002,
+  author       = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas and Schnoebelen, Philippe},
+  title        = {Temporal logic with forgettable past},
+  booktitle    = {Logic in Computer Science, 2002. Proceedings. 17th Annual IEEE Symposium on},
+  year         = {2002},
+  organization = {IEEE},
+  pages        = {383--392},
+}
+
+@Book{Prior1957,
+  author    = {Prior, Arthur N},
+  title     = {Time and modality},
+  year      = {1957},
+  publisher = {Clarendon Press},
+}