blob: a888df8f776ad2e2dce5ae340d03e2dade76e722 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
\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
|
