Merge branch 'master' of gitlab.science.ru.nl:eveen/Model-Checking

1 files changed, 3 insertions, 2 deletions

diff --git a/Assignment1/intro.tex b/Assignment1/intro.tex
index d07be86..ddbaa5a 100644
--- a/Assignment1/intro.tex
+++ b/Assignment1/intro.tex
@@ -1,8 +1,8 @@
+\erin
 \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
-\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.
@@ -17,7 +17,8 @@ Eventually, formal computing scientists stopped using past modalities for reason
 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.}
+	\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.
+		(Like the book, this section may contain typos and inaccuracies. These are however not intentional.)}
 	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.