summaryrefslogtreecommitdiff
path: root/Assignment1/conversion.tex
diff options
context:
space:
mode:
authorCamil Staps2018-04-18 16:53:14 +0200
committerCamil Staps2018-04-18 16:53:14 +0200
commitd256a2eec6f958db99e2d11ab81d25a351009a30 (patch)
tree766ca6f9c708665484482c325b3fe1b5cf85e58f /Assignment1/conversion.tex
parentfinish conversion example (diff)
Finish(?) SSH example
Diffstat (limited to 'Assignment1/conversion.tex')
-rw-r--r--Assignment1/conversion.tex4
1 files changed, 2 insertions, 2 deletions
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 9d956b6..72304d2 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -145,6 +145,7 @@ The final step of the algorithm entails removing the parts of the formula that c
\camil
\begin{example}[Properties for an Authentication System]
+ \label{ex:pltl-to-ltl:authentication}
Consider again the property from \cref{ex:pltl:authentication-system}, repeated here with less verbose names:
$\phi = \square (c \rightarrow \lnot f \Sop s)$.
This can be rewritten to a form with only $\Uop$ and $\Sop$:
@@ -254,8 +255,7 @@ The final step of the algorithm entails removing the parts of the formula that c
\item $\square\lnot(f \land \psi)$.
After an authentication failure, a connection cannot be established without prior authentication success.
\end{itemize}
- We see that the formula is reasonably succinct compared to its PLTL version, $\square(c \rightarrow \lnot f \Sop s)$.
- Using past modalities was not needed in this case.
+ The resulting LTL formula is reasonably succinct, but is clear that the PLTL formula is easier to construct and understand.
\end{example}
\erin