diff options
Diffstat (limited to 'Assignment1/semantics.tex')
| -rw-r--r-- | Assignment1/semantics.tex | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Assignment1/semantics.tex b/Assignment1/semantics.tex index 7840cef..055d66b 100644 --- a/Assignment1/semantics.tex +++ b/Assignment1/semantics.tex @@ -17,6 +17,7 @@ We use $\sigma \vDash \phi$ as a shorthand for $\sigma \vDash_0 \phi$. \erin \begin{definition}[Semantics of PLTL (Interpretation over Words)] + \label{def:pltl:semantics-words} Let $\phi$ be a PLTL formula over $AP$. The LT property induced by $\phi$ is \[Words(\phi) = \{\sigma \in \left(2^{AP}\right)^\omega \mid \sigma \vDash \phi\}\] where $\vDash\ \subseteq \left(2^{AP}\right)^\omega \times \mathbb{N} \times PLTL$ is the smallest relation with the properties in \cref{fig:PLTL-semantics}. @@ -40,7 +41,7 @@ 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 \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\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$} \end{matrix*} |