\erin
\subsection{Past Modalities in LTL}\label{sec:intro}
As mentioned in Remark 5.16, LTL can be extended with \emph{past modalities}.
This section discusses this extension.
The combination of LTL and Past Modalities is often called \enquote{LTL-Past} or PLTL; we will use the second.
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.
The complexity of the model problem does not increase with this extension~\citep{Sistla1985},
	but neither does the expressiveness of the system compared to LTL~\citep{Gabbay1980}.
Eventually, formal computing scientists stopped using past modalities for reasons of minimality.

\erin
In 2003, Nicolas Markey showed that while past modalities do not increase expressive power,
they can make LTL formulas exponentially more succinct~\cite{Markey2003}.
In other words, there is a class of PLTL formulae%
	\footnote{In keeping with the style of the rest of the book, we alternate between \enquote{formulas} and \enquote{formulae} and wish the reader best of luck with this.
		(Like the book, this section may contain typos and inaccuracies. These are however not intentional.)}
	for which the size of all equivalent LTL formulas is $\Omega\left(2^n\right)$.
Markey achieves this proof by providing a formula that is in exactly this class.
Besides being smaller, PLTL formulas can also be easier to write and understand, as examples below will demonstrate.
They are also included in many model checking tools, such as NuSMV,\footnote{\url{http://nusmv.fbk.eu/}}, and as we will see in the examples they are used in practice.
For this reason, it is useful to discuss them here.