\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