\camil
\subsection{Summary}
\emph{NB: these points are to be added to the current section 5.3.}
\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.

	\item
		For PLTL, there are two different notions of equivalence.
		Initial equivalence $\phi \equiv_0 \psi$ means that all paths that satisfy $\phi$ in position 0 must also satisfy $\psi$ in position 0 (and vice versa).
		Equivalence $\phi \equiv \psi$ means that for all paths $\pi$ and positions $i$, $\pi \vDash_i \phi$ entails $\pi \vDash_i \psi$ (and vice versa).

	\item
		Because past modalities do not increase expressiveness, PLTL formulas can be translated into initially equivalent LTL formulas.
		This can be done with syntactic rewrite rules or with a conversion through B\"uchi automata and Muller automata.

	\item
		If $vw^\omega$ is a counterexample for a safety property $P$ in a finite transition system $TS$, there exists a $j \le |TS|\cdot2^{|\lnot P|}\cdot|\lnot P|$ for which $vw^j$ is a bad prefix for $P$.
		However, in most cases a smaller counterexample (not of the form $vw^k$) can be found by translating $P$ to a finite automaton and running it with $vw^\omega$.
\end{itemize}
\cbend