\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