Finish semantics example

2 files changed, 19 insertions, 3 deletions

diff --git a/Assignment1/equivalence.tex b/Assignment1/equivalence.tex
index 6195afc..6373088 100644
--- a/Assignment1/equivalence.tex
+++ b/Assignment1/equivalence.tex
@@ -8,9 +8,12 @@ we can define equivalence on PLTL formulas.
 	\[\text{for any path } \pi \text{ and any position } i, \pi \vDash_i \phi \Leftrightarrow \pi \vDash_i \psi \qedhere\]
 \end{definition}
 
-Additionally, we can define another form of equivalence, initial equivalence:
+Additionally, we can define another form of equivalence, initial equivalence.
+When two formulas are initially equivalent, they are equivalent for all paths at position 0.
+This is mainly useful to compare PLTL and LTL formulas.
 \begin{definition}[Initial Equivalence of PLTL Formulae]
 	PLTL formulae $\phi_1,\phi_2$ are initially equivalent, denoted $\phi_1 \equiv_0 \phi_2$ iff they verify the following property:
 	\[\text{for any path } \pi, \pi \vDash_0 \phi \Leftrightarrow \pi \vDash_0 \psi \qedhere\]
 \end{definition}
 \cbend
+%TODO: examples
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