diff options
| -rw-r--r-- | Assignment1/bad-prefix.tex | 1 | ||||
| -rw-r--r-- | Assignment1/conversion.tex | 26 | ||||
| -rw-r--r-- | Assignment1/exercises.tex | 1 | ||||
| -rw-r--r-- | Assignment1/syntax.tex | 26 |
4 files changed, 48 insertions, 6 deletions
diff --git a/Assignment1/bad-prefix.tex b/Assignment1/bad-prefix.tex index a2101ba..c9145b3 100644 --- a/Assignment1/bad-prefix.tex +++ b/Assignment1/bad-prefix.tex @@ -25,6 +25,7 @@ Once a state reoccurs, $j$ is found. This algorithm, more formally described in \cref{alg:bad-prefix}, is obviously guaranteed to find the smallest $i,j$ for which $vw^i$ and $vw^j$ lead to the same state. However, it is not guaranteed to find a minimal bad prefix (for instance, when a prefix of $v$ already is a minimal bad prefix). +% TODO: fix placement; see https://tex.stackexchange.com/q/427278/23992 \begin{algorithm}[H] % NOTE: ugly hardcoded spacing to mimic ugly algorithm layout by Baier-Katoen \caption{Finding a bad prefix for a safety property from a counterexample $vw^\omega$} 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 diff --git a/Assignment1/exercises.tex b/Assignment1/exercises.tex index 647755e..ba056d5 100644 --- a/Assignment1/exercises.tex +++ b/Assignment1/exercises.tex @@ -64,6 +64,7 @@ \end{exercise} \begin{exercise} + \label{ex:succinctness} In this exercise we prove that PLTL formulas can be exponentially more succinct. The proof followed here is that of \citet{Markey2003} which, in turn, is based on work by \citet{Etessami2002}. The proof is achieved by giving an example of a formula which can be expressed in $\mathcal O(n)$ in PLTL but requires $\Omega(n)$ in LTL. diff --git a/Assignment1/syntax.tex b/Assignment1/syntax.tex index 3f3430c..7ffa813 100644 --- a/Assignment1/syntax.tex +++ b/Assignment1/syntax.tex @@ -185,13 +185,29 @@ Before turning to the formal semantics in the next subsection, we provide some e The LTL formula is slightly larger than the PLTL formula and is slightly less understandable. \end{example} +\begin{example}[Protocol Dependencies] + \label{ex:pltl:protocol-dependencies} + Past modalities can be useful to describe a protocol in which messages have dependencies. + For example, the Secure Shell (SSH) protocol requires that keys have been exchanged between two machines before an authentication request can be handled: + if authentication is handled before keys are exchanged, the communication could be intercepted, leaking login details. + On an abstract level, there are formulas $\phi_1,\dots,\phi_n,\psi$ and $\psi$ should only hold if $\phi_1,\dots,\phi_n$ held previously (and in that order). + In the case of SSH, $\psi$ is the handling of an authentication request; + $\phi_1,\dots,\phi_n$ indicate that keys are exchanged correctly. + \citet{FiterauBrostean2017} modelled this property using the $\lozenge^{-1}$ modality, which can easily model this dependency. + It is here given for $n=3$ (as is the case for SSH): + \[ + \square \big(\psi \rightarrow + \lozenge^{-1} (\phi_3 \land + \lozenge^{-1} (\phi_2 \land + \lozenge^{-1} \phi_1))\big) + \] +\end{example} + \begin{remark}[Other Notations] - % TODO: I don't find this place logical for this remark, but it is the same place as Remark 5.16 in the book. Like for LTL, many different notations are used in literature for PLTL. These include - $\mathbf X^{-1}, \mathbf G^{-1}, \mathbf F^{-1}$~\citep[e.g.]{Markey2003}, - but also \raisebox{-1pt}{\tikz\draw[black,fill=black](0,0)circle(.4em);}$,\blacksquare,\blacklozenge$~\citep[e.g.]{Gabbay1989} - or $\stackinset{c}{}{c}{}{$\cdot$}{$\bigcirc$},\boxdot,\stackinset{c}{}{c}{}{$\cdot$}{$\lozenge$}$~\citep[e.g.]{Havelund2002}. - % It is always fun to come up with new versions and watch people struggling to reproduce them in \LaTeX. + $\mathbf X^{-1}, \mathbf G^{-1}, \mathbf F^{-1}$~\citep{Markey2003}, + but also \raisebox{-1pt}{\tikz\draw[black,fill=black](0,0)circle(.4em);}$,\blacksquare,\blacklozenge$~\citep{Gabbay1989} + and $\stackinset{c}{}{c}{}{$\cdot$}{$\bigcirc$},\boxdot,\stackinset{c}{}{c}{}{$\cdot$}{$\lozenge$}$~\citep{Havelund2002}. \end{remark} \cbend |