Example: protocol dependencies

1 files changed, 25 insertions, 1 deletions

diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 4feb094..75ac71f 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -91,7 +91,7 @@ For the proofs of the equivalences, we refer the reader to the appendix of \cite
 
 \erin
 \begin{enumerate}[resume]
-	\item Suppose $E = q \Sop (a \wedge \neg (\alpha \Uop \beta))$, then $E \equiv E_1 \vee E_2 \vee E_3$ where:
+	\item Suppose $E = (q \lor \alpha\Uop\beta) \Sop a$, then $E \equiv E_1 \vee E_2 \vee E_3$ where:
 		\begin{align*}
 			E_1 &= \bot \Sop a\\
 			E_2 &= (\beta \lor \alpha \land \alpha \Uop \beta) \land (\neg a \lor \neg c) \Sop a\\
@@ -268,6 +268,30 @@ After all, these formulas are meaningless for $\vDash_0$, since (using Gabbay's
 			After an authentication failure, a connection cannot be established without prior authentication success.
 	\end{itemize}
 	The resulting LTL formula is reasonably succinct, but is clear that the PLTL formula is easier to construct and understand.
+
+	Note that we have not proven that no smaller LTL formula exists.
+	For an example of such a proof, see \cref{ex:succinctness}.
+\end{example}
+
+\begin{example}[Protocol Dependencies]
+	In \cref{ex:pltl:protocol-dependencies}, we considered the PLTL formula
+	$\square \big(\psi \rightarrow
+			\lozenge^{-1} (\phi_3 \land
+				\lozenge^{-1} (\phi_2 \land
+					\lozenge^{-1} \phi_1))\big)$.
+	By the definitions of $\square$ and $\lozenge^{-1}$, it is equivalent to
+	\[
+		\lnot\big(
+			\top \Uop (
+				\psi \land \lnot (
+					\top \Sop (
+						\phi_3 \land \top \Sop (\phi_2 \land \top \Sop \phi_1)
+		)))\big).
+	\]
+	No other temporal operators besides $\Uop$ and $\Sop$ are used, so to transform it to an initially equivalent LTL formula step 1 is not needed.
+
+	Rewriting the formula to Gabbay's definitions and separating the pure past formulas in step 2 proceeds as in the previous example.
+	The exact steps are not shown here for reasons of brevity.
 \end{example}
 
 \erin