diff options
Diffstat (limited to 'Assignment1/semantics.tex')
| -rw-r--r-- | Assignment1/semantics.tex | 40 |
1 files changed, 31 insertions, 9 deletions
diff --git a/Assignment1/semantics.tex b/Assignment1/semantics.tex index f851b14..791eb15 100644 --- a/Assignment1/semantics.tex +++ b/Assignment1/semantics.tex @@ -35,7 +35,7 @@ The information about $A_0$ is not lost, so whether $\bigcirc\phi$ holds for $\s \begin{mdframed} \[ \begin{matrix*}[l] - \sigma &\vDash_i & \text{true}\\ + \sigma &\vDash_i & \top\\ \sigma &\vDash_i & a &\text{iff} & a\in A_i\\ \sigma &\vDash_i & \phi_1\land\phi_2 &\text{iff} & \text{$\sigma\vDash_i\phi_1$ and $\sigma\vDash_i\phi_2$}\\ \sigma &\vDash_i & \lnot\phi &\text{iff} & \sigma \nvDash_i \phi\\ @@ -51,6 +51,35 @@ The information about $A_0$ is not lost, so whether $\bigcirc\phi$ holds for $\s \end{figure} \erin +Given these definitions, it is possible to derive the formal semantics of the $\Fop^{-1}$ and $\Gop^{-1}$ operators as well: +\[ + \begin{matrix*}[l] + \sigma &\vDash_i &\Fop^{-1}\phi &\text{iff} &\exists_{0 \leq j \leq i}[\sigma \vDash_j \phi]\\ + \sigma &\vDash_i &\Gop^{-1}\phi &\text{iff} &\forall_{0 \leq j \leq i}[\sigma \vDash_j \phi] + \end{matrix*} +\] +\camil +The first follows from the rule for $\Sop$ and the fact that $\sigma \vDash_i \top$ for all $i\in\mathbb N$. +The second follows from: +\begin{align*} + \sigma \vDash_i \square^{-1}\phi + &\quad\Leftrightarrow\quad \sigma \vDash_i \lnot\lozenge^{-1}\lnot\phi\\ + &\quad\Leftrightarrow\quad \sigma \nvDash_i \lozenge^{-1}\lnot\phi\\ + &\quad\Leftrightarrow\quad \nexists_{0\le j\le i} [\sigma \vDash_j \lnot\phi]\\ + &\quad\Leftrightarrow\quad \forall_{0\le j\le i} [\sigma \vDash_j \phi]. +\end{align*} + +With this result we can also derive the semantics of the dual modalities $\lozenge^{-1}\square^{-1}$ and $\square^{-1}\lozenge^{-1}$: +\[ + \sigma \vDash_i \lozenge^{-1}\square^{-1}\phi + \quad\Leftrightarrow\quad + \sigma \vDash_i \square^{-1}\lozenge^{-1}\phi + \quad\Leftrightarrow\quad + \sigma \vDash_0 \phi +\] +This is done in \cref{ex:dual-modalities}. + +\erin \begin{definition}[Semantics of PLTL over Paths and States] Let $TS = (S, Act, \rightarrow, I, AP, L)$ be a transition system without terminal states, and let $\phi$ be an PLTL-formula over AP. \begin{itemize} @@ -66,11 +95,4 @@ In order to make these definitions suitable for use with our PLTL operators, we must provide their semantics. \Cref{fig:PLTL-semantics} shows the formal semantics of the operators defined in the grammar. Note that we need to add a index $i$, since we must also be able to look in the past. - -Given these definitions, it is possible to derive the formal semantics of the $\Fop^{-1}$ and $\Gop^{-1}$ operators as well: -\[ - \begin{matrix*}[l] - \sigma &\vDash_i &\Fop^{-1}\phi &\text{iff} &\exists_{0 \leq k \leq i}[\sigma \vDash_k \phi]\\ - \sigma &\vDash_i &\Gop^{-1}\phi &\text{iff} &\forall_{0 \leq k \leq i}[\sigma \vDash_k \phi] - \end{matrix*} -\] +\cbend |