summaryrefslogtreecommitdiff
path: root/Assignment1/conversion.tex
diff options
context:
space:
mode:
authorCamil Staps2018-04-18 21:48:33 +0200
committerCamil Staps2018-04-18 21:48:33 +0200
commit25ffc622afc727baa7c5c2918ee602b98bb291a3 (patch)
treef1bffb5db779cc505c70892b91acdfc3e13f24dc /Assignment1/conversion.tex
parentBars everywhere (diff)
Example: protocol dependencies
Diffstat (limited to 'Assignment1/conversion.tex')
-rw-r--r--Assignment1/conversion.tex26
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