diff options
author | Camil Staps | 2018-04-18 21:48:33 +0200 |
---|---|---|
committer | Camil Staps | 2018-04-18 21:48:33 +0200 |
commit | 25ffc622afc727baa7c5c2918ee602b98bb291a3 (patch) | |
tree | f1bffb5db779cc505c70892b91acdfc3e13f24dc /Assignment1/conversion.tex | |
parent | Bars everywhere (diff) |
Example: protocol dependencies
Diffstat (limited to 'Assignment1/conversion.tex')
-rw-r--r-- | Assignment1/conversion.tex | 26 |
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 |