diff options
Diffstat (limited to 'Assignment1/semantics.tex')
| -rw-r--r-- | Assignment1/semantics.tex | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/Assignment1/semantics.tex b/Assignment1/semantics.tex index 1bca0b2..d99e636 100644 --- a/Assignment1/semantics.tex +++ b/Assignment1/semantics.tex @@ -117,7 +117,20 @@ The only difference is that $\vDash$ now is a ternary relation, and we use $\pi\ \end{figure} \begin{example}[Satisfaction of PLTL Formulae by Transition Systems] - Consider again the transition system from Figure 5.3, reproduced as \cref{fig:pltl:example-ts}. - % TODO + Consider again the transition system $TS$ from Figure 5.3, reproduced as \cref{fig:pltl:example-ts}. + \begin{itemize} + \item + Recall that $TS \vDash \square a$. + A noteworthy peculiarity is that $TS \nvDash \square\Xop^{-1}a$, since $\Xop^{-1}\phi$ is always false at position 0. + Clearly, we do have $TS \vDash_i \square\Xop^{-1}a$ for $i \ge 1$. + \item + We also have $TS \vDash \square(b \rightarrow \square^{-1}b)$. + After all, if $b$ does not hold, $b$ will never hold again. + \item + We have $s_1 \vDash \square(a \Sop b)$: + since $a$ always holds, this is for $TS$ equivalent to $\square(\top \Sop b) \equiv \square(\lozenge^{-1}b)$, and $s_1 \vDash b$. + However, since $s_2 \nvDash \square(a \Sop b)$ (because $a^\omega \nvDash \square(a \Sop b)$), also $TS \nvDash \square(a \Sop b)$. + \qedhere + \end{itemize} \end{example} \cbend |