diff options
Diffstat (limited to 'Assignment1/semantics.tex')
| -rw-r--r-- | Assignment1/semantics.tex | 40 |
1 files changed, 39 insertions, 1 deletions
diff --git a/Assignment1/semantics.tex b/Assignment1/semantics.tex index 055d66b..dcc8e6b 100644 --- a/Assignment1/semantics.tex +++ b/Assignment1/semantics.tex @@ -51,6 +51,23 @@ The information about $A_0$ is not lost, so whether $\bigcirc\phi$ holds for $\s \label{fig:PLTL-semantics} \end{figure} +\begin{example}[Satisfaction of PLTL Formulae by Words] + Let $\pi = aabcdcdcd\dots$ be an infinite path over $AP=\{a,b,c,d\}$, of which on every moment only one atomic proposition holds (i.e., at position 0, $a$ holds, at position 2, $b$ holds, etc.). + We have for instance: + + \begin{itemize} + \item For all $i\in\mathbb N$, $\pi \vDash_i b \rightarrow \Xop^{-1}a$. + If $i \ne 2$, $b$ does not hold and the implication is trivially satisfied. + If $i = 2$, we have $\pi \vDash_{i-1} a$ and the formula is satisfied as well. + \item For all $i\ge 2$, $\pi \vDash_i (d \rightarrow \Xop^{-1} c) \Sop b$. + We need to give $0 \le j \le i$ with $\pi \vDash_j b$ and $\pi \vDash_k d \rightarrow \Xop^{-1} c$ for all $j < k \le i$. + Clearly, we can only give $j=2$. + Then for odd positions $k$, the implication $d \rightarrow \Xop^{-1} c$ holds trivially since $d$ does not hold. + For even positions $k$, it holds as well since $c$ holds at odd positions $n > 2$. + \qedhere + \end{itemize} +\end{example} + \erin Given these definitions, it is possible to derive the formal semantics of the $\Fop^{-1}$ and $\Gop^{-1}$ operators as well: \[ @@ -59,6 +76,7 @@ Given these definitions, it is possible to derive the formal semantics of the $\ \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: @@ -81,5 +99,25 @@ With this result we can also derive the semantics of the dual modalities $\lozen This is done in \cref{ex:dual-modalities}. The semantics over words extend to transition systems similar to the LTL case in Definition 5.7. -The only difference is that $\vDash$ now is a ternary relation, and we use $\vDash$ as shorthand for $\vDash_0$. +The only difference is that $\vDash$ now is a ternary relation, and we use $\pi\vDash\phi$ as a shorthand for $\pi\vDash_0\phi$. + +\begin{figure}[h] + \centering + \begin{tikzpicture}[initial text={},node distance=3cm,->] + \node[state,label=below:{$\{a,b\}$},initial] (s1) {$s_1$}; + \node[state,label=below:{$\{a,b\}$},right of=s1] (s2) {$s_2$}; + \node[state,label=below:{$\{a\}$},right of=s2,initial right] (s3) {$s_3$}; + \draw (s1) edge[bend left] (s2); + \draw (s2) edge[bend left] (s1); + \draw (s2) -- (s3); + \draw (s3) edge[loop above,looseness=8,in=60,out=120] (s3); + \end{tikzpicture} + \caption{Example for semantics of PLTL.} + \label{fig:pltl:example-ts} +\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 +\end{example} \cbend |