diff options
Diffstat (limited to 'Assignment1/intro.tex')
| -rw-r--r-- | Assignment1/intro.tex | 9 |
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. |