diff options
| author | Erin van der Veen | 2018-04-09 17:15:43 +0200 |
|---|---|---|
| committer | Erin van der Veen | 2018-04-09 17:15:43 +0200 |
| commit | b5fde0437d3dc248927e99af4a4a35f55b36c499 (patch) | |
| tree | 36e082606821c01fd36116b8c7d6fc661f269c3b /Assignment1/assignment1.tex | |
| parent | Formal semantics of LTLP (diff) | |
LTL-Past -> LTLP
Diffstat (limited to 'Assignment1/assignment1.tex')
| -rw-r--r-- | Assignment1/assignment1.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex index 842047c..1994cf1 100644 --- a/Assignment1/assignment1.tex +++ b/Assignment1/assignment1.tex @@ -33,7 +33,7 @@ %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. +for the sake of brevity we will use the second (LTLP) 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}, |