From 3d377ca8fbe6492f5b1faf38c09160939e36d711 Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Thu, 19 Apr 2018 18:33:07 +0200
Subject: Example for satisfaction by words; still needed: satisfaction by TS
 (and equivalence)

---
 Assignment1/semantics.tex | 40 +++++++++++++++++++++++++++++++++++++++-
 1 file changed, 39 insertions(+), 1 deletion(-)

(limited to 'Assignment1/semantics.tex')

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
-- 
cgit v1.2.3

