diff options
Diffstat (limited to 'Assignment1/semantics.tex')
| -rw-r--r-- | Assignment1/semantics.tex | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/Assignment1/semantics.tex b/Assignment1/semantics.tex index dcc8e6b..1bca0b2 100644 --- a/Assignment1/semantics.tex +++ b/Assignment1/semantics.tex @@ -24,12 +24,12 @@ We use $\sigma \vDash \phi$ as a shorthand for $\sigma \vDash_0 \phi$. \end{definition} \camil Note that we must redefine the satisfaction relation for the LTL operators, because $\vDash$ is now a ternary relation. -The difference with LTL formulae is well illustrated by the $\bigcirc$ operator. -In the LTL case, $\sigma=A_0A_1A_2\dots\vDash\bigcirc\phi$ iff $\sigma[1\dots]=A_1A_2\dots\vDash\phi$. -Thus, whether $\bigcirc\phi$ holds for $\sigma$ cannot depend on $A_0$. -In the PLTL case, $\sigma\vDash_i\bigcirc\phi$ iff $\sigma\vDash_{i+1}\phi$. -The information about $A_0$ is not lost, so whether $\bigcirc\phi$ holds for $\sigma$ may depend on $A_0$, - as is trivially the case with $\bigcirc\bigcirc^{-1}a$. +The difference with LTL formulae is well illustrated by the $\Xop$ operator. +In the LTL case, $\sigma=A_0A_1A_2\dots\vDash\Xop\phi$ iff $\sigma[1\dots]=A_1A_2\dots\vDash\phi$. +Thus, whether $\Xop\phi$ holds for $\sigma$ cannot depend on $A_0$. +In the PLTL case, $\sigma\vDash_i\Xop\phi$ iff $\sigma\vDash_{i+1}\phi$. +The information about $A_0$ is not lost, so whether $\Xop\phi$ holds for $\sigma$ may depend on $A_0$, + as is trivially the case with $\Xop\Xop^{-1}a$. \begin{figure} \centering @@ -40,7 +40,7 @@ The information about $A_0$ is not lost, so whether $\bigcirc\phi$ holds for $\s \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\\ - \sigma &\vDash_i & \bigcirc\phi &\text{iff} & \sigma \vDash_{i+1} \phi\\ + \sigma &\vDash_i & \Xop\phi &\text{iff} & \sigma \vDash_{i+1} \phi\\ \sigma &\vDash_i & \phi_1\Uop\phi_2 &\text{iff} & \exists_{j \ge i}.\text{$\sigma \vDash_j \phi_2$ and $\sigma \vDash_k \phi_1$ for all $i \le k < 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$} |