diff options
Diffstat (limited to 'Assignment1/syntax.tex')
| -rw-r--r-- | Assignment1/syntax.tex | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Assignment1/syntax.tex b/Assignment1/syntax.tex index babf688..6fc0002 100644 --- a/Assignment1/syntax.tex +++ b/Assignment1/syntax.tex @@ -117,6 +117,7 @@ we include an arrow that points to the state for which the formula holds. \end{figure} \camil +\label{pltl:dual-modalities} Dual modalities, like the LTL $\square\lozenge$ \enquote{infinitely often} and \enquote{eventually forever}, are less useful in PLTL. $\square^{-1}\lozenge^{-1}\phi$ intuitively holds when at every point in the past, $\phi$ held or there was a previous moment at which $\phi$ held. This is satisfied precisely when $\phi$ held at the first moment in time. |