diff options
| -rw-r--r-- | Assignment1/bad-prefix.tex | 1 | ||||
| -rw-r--r-- | Assignment1/intro.tex | 9 | ||||
| -rw-r--r-- | Assignment1/summary.tex | 1 |
3 files changed, 2 insertions, 9 deletions
diff --git a/Assignment1/bad-prefix.tex b/Assignment1/bad-prefix.tex index c9145b3..e357359 100644 --- a/Assignment1/bad-prefix.tex +++ b/Assignment1/bad-prefix.tex @@ -1,6 +1,5 @@ \camil \subsection{Minimal Bad Prefixes} -%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? \emph{NB: this section is not particularly about PLTL. It is better added as 4.4.3.} Model checking tools, such as NuSMV, often give counterexamples in the form of $vw^\omega$, i.e., a finite prefix with a infinite loop. 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. diff --git a/Assignment1/summary.tex b/Assignment1/summary.tex index 31b65f8..ef9f458 100644 --- a/Assignment1/summary.tex +++ b/Assignment1/summary.tex @@ -1,6 +1,5 @@ \camil \subsection{Summary} -% TODO: points to be added to 5.3 \emph{NB: these points are to be added to the current section 5.3.} \begin{itemize} \item |