From 8fea3daf5daf8100a1617ab500f8860c977e2cba Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Sun, 15 Apr 2018 12:25:14 +0200
Subject: Add two summary points, this means we do not need a comparison
 subsection any more

---
 Assignment1/summary.tex | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'Assignment1/summary.tex')

diff --git a/Assignment1/summary.tex b/Assignment1/summary.tex
index 6f243b2..a888df8 100644
--- a/Assignment1/summary.tex
+++ b/Assignment1/summary.tex
@@ -1,2 +1,14 @@
 \subsection{Summary}
 % TODO: points to be added to 5.3
+\camil
+\begin{itemize}
+	\item
+		PLTL is an extension to LTL which adds \emph{past modalities}.
+		The extension is not more expressive, but PLTL formulas can be exponentially more succinct than their LTL equivalents.
+
+	\item
+		Because PLTL formulas need to be able to \enquote{look back}, the satisfaction relation $\vDash$ becomes ternary:
+			it is a subset of $\left(2^{AP}\right)^\omega \times \mathbb N \times PLTL$,
+			where the natural number indicates the index at which a trace satisfies a formula.
+\end{itemize}
+\cbend
-- 
cgit v1.2.3