blob: d18e517e3a067409799725d0b1c7f3a32b7f9352 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
\camil
\subsection{Summary}
% TODO: points to be added to 5.3
\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.
\end{itemize}
\cbend
|
