Minor textual enhancements; remove outdated todos

1 files changed, 2 insertions, 7 deletions

diff --git a/Assignment1/intro.tex b/Assignment1/intro.tex
index ddbaa5a..fb2255e 100644
--- a/Assignment1/intro.tex
+++ b/Assignment1/intro.tex
@@ -1,12 +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
 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.
+The combination of LTL and Past Modalities is often called \enquote{LTL-Past} or PLTL; we will use the second.
 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.
 The complexity of the model problem does not increase with this extension~\citep{Sistla1985},
@@ -22,6 +18,5 @@ In other words, there is a class of PLTL formulae%
 	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.%
-	\footnote{\url{http://nusmv.fbk.eu/}}
+They are also included in many model checking tools, such as NuSMV,\footnote{\url{http://nusmv.fbk.eu/}}, and as we will see in the examples they are used in practice.
 For this reason, it is useful to discuss them here.