diff options
Diffstat (limited to 'Assignment1/semantics.tex')
| -rw-r--r-- | Assignment1/semantics.tex | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/Assignment1/semantics.tex b/Assignment1/semantics.tex index 43942b5..f851b14 100644 --- a/Assignment1/semantics.tex +++ b/Assignment1/semantics.tex @@ -40,9 +40,9 @@ The information about $A_0$ is not lost, so whether $\bigcirc\phi$ holds for $\s \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\\ \sigma &\vDash_i & \bigcirc\phi &\text{iff} & \sigma \vDash_{i+1} \phi\\ - \sigma &\vDash_i & \phi_1\Uop\phi_2 &\text{iff} & \exists_{j \le 0}.\text{$\sigma \vDash_j \phi_2$ and $\sigma \vDash_i \phi_1$ for all $0 \le i < j$}\\ - \sigma &\vDash_i & \phi_1\Sop\phi_2 &\text{iff} & \exists_{j \le i}.\text{$\sigma \vDash_j \phi_2$ and $\sigma \vDash_k \phi_1$ for all $j < k \le i$}\\ - \sigma &\vDash_i & \Pop\phi &\text{iff} & i \geq 1 \wedge \sigma \vDash_{i-1} \phi + \sigma &\vDash_i & \phi_1\Uop\phi_2 &\text{iff} & \exists_{j \ge 0}.\text{$\sigma \vDash_j \phi_2$ and $\sigma \vDash_i \phi_1$ for all $0 \le i < j$}\\ + \sigma &\vDash_i & \phi_1\Sop\phi_2 &\text{iff} & \exists_{0 \le j \le i}.\text{$\sigma \vDash_j \phi_2$ and $\sigma \vDash_k \phi_1$ for all $j < k \le i$}\\ + \sigma &\vDash_i & \Pop\phi &\text{iff} & \text{$i \geq 1$ and $\sigma \vDash_{i-1} \phi$} \end{matrix*} \] \end{mdframed} @@ -70,7 +70,7 @@ Note that we need to add a index $i$, since we must also be able to look in the 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_{k \leq i}[\sigma \vDash_k \phi]\\ - \sigma &\vDash_i &\Gop^{-1}\phi &\text{iff} &\forall_{k \leq i}[\sigma \vDash_k \phi] + \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*} \] |