From d256a2eec6f958db99e2d11ab81d25a351009a30 Mon Sep 17 00:00:00 2001 From: Camil Staps Date: Wed, 18 Apr 2018 16:53:14 +0200 Subject: Finish(?) SSH example --- Assignment1/conversion.tex | 4 ++-- Assignment1/syntax.tex | 14 ++++++-------- 2 files changed, 8 insertions(+), 10 deletions(-) (limited to 'Assignment1') 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 diff --git a/Assignment1/syntax.tex b/Assignment1/syntax.tex index 42ebf63..8543669 100644 --- a/Assignment1/syntax.tex +++ b/Assignment1/syntax.tex @@ -170,13 +170,11 @@ Before turning to the formal semantics in the next subsection, we provide some e One property says that if a channel is opened, there must have been some successful authentication attempt in the past~\citep[p.~149]{FiterauBrostean2017}. Also, since that successful authentication, no authentication failure must have occurred. This formula is intuitively expressed by $\square(\textsl{hasOpenedChannel} \rightarrow \lnot \textsl{authFailure} \Sop \textsl{authSuccess})$. - Expressing this property in LTL is obscure and tedious. - One way uses the Weak Until operator from Section 5.1.5: - %TODO please check that this is actually equivalent - \begin{align*} - & \lnot \textsl{hasOpenedChannel} \Wop\\ - & \quad (\textsl{authSuccess} \land (\square \textsl{authFailure} \rightarrow \lnot \textsl{hasOpenedChannel} \Uop \textsl{authSuccess})) - \qedhere - \end{align*} + An equivalent LTL formula is $\lnot \psi \land \square\lnot(\textsl{authFailure} \land \psi)$, + where $\psi = \lnot\textsl{authSuccess} \Uop (\textsl{hasOpenedChannel} \land \lnot\textsl{authSuccess})$. + If $\psi$ holds, a channel will be opened without prior authentication success. + Therefore, $\psi$ should not hold at the beginning or when authentication fails. + The LTL formula is derived algorithmically in \cref{ex:pltl-to-ltl:authentication}. + The LTL formula is slightly larger than the PLTL formula and is slightly less understandable. \end{example} \cbend -- cgit v1.2.3 From 32f1f4867bad79eb4d5afd179697b92699521698 Mon Sep 17 00:00:00 2001 From: Camil Staps Date: Wed, 18 Apr 2018 19:33:40 +0200 Subject: Minor enhancements --- Assignment1/assignment1.tex | 1 - Assignment1/conversion.tex | 5 +++-- Assignment1/intro.tex | 3 ++- Assignment1/specifying-properties.tex | 13 ------------- Assignment1/syntax.tex | 30 ++++++++++++++++++++++-------- 5 files changed, 27 insertions(+), 25 deletions(-) delete mode 100644 Assignment1/specifying-properties.tex (limited to 'Assignment1') diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex index 1e5a55a..e8e34dd 100644 --- a/Assignment1/assignment1.tex +++ b/Assignment1/assignment1.tex @@ -111,7 +111,6 @@ \input{intro} \input{syntax} \input{semantics} -\input{specifying-properties} \input{equivalence} \input{conversion} %TODO: (Section?) Assess if PLTL is actually more succinct using the examples from the SSH Paper diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex index 72304d2..3f4cf0f 100644 --- a/Assignment1/conversion.tex +++ b/Assignment1/conversion.tex @@ -7,6 +7,7 @@ The second algorithm makes use of the translation of PLTL formulas to automata a This algorithm is described in more detail below. \paragraph{Syntactic Algorithm} +\label{pltl:to-ltl:syntactic} The syntactic algorithm as proposed by Gabbay has its foundation in the following three facts:% \footnote{% Note that Gabbay used a slightly different, \enquote{non-strict} definition for the $\Uop$ and $\Sop$ operators. @@ -144,7 +145,7 @@ These equivalences also hold when the path is reversed, so similar elimination r The final step of the algorithm entails removing the parts of the formula that contains the $\Sop$-operators. \camil -\begin{example}[Properties for an Authentication System] +\begin{example}[A property 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)$. @@ -338,8 +339,8 @@ Let us first define the Muller Automaton: Converting a NBA to a Muller automaton was shown to be possible by R. McNaughton~\cite{McNaughton1966} and is part of what is known as McNaughton's theorem. - \cbend + %Provide the syntactic algorithm to convert PLTL to LTL %TODO: Provide algorithm via automata to convert PLTL to LTL %TODO: In both cases make use of examples from SSH Paper diff --git a/Assignment1/intro.tex b/Assignment1/intro.tex index d07be86..15294ee 100644 --- a/Assignment1/intro.tex +++ b/Assignment1/intro.tex @@ -17,7 +17,8 @@ Eventually, formal computing scientists stopped using past modalities for reason In 2003, Nicolas Markey showed that while past modalities do not increase expressive power, they can make LTL formulas exponentially more succinct~\cite{Markey2003}. In other words, there is a class of PLTL formulae% - \footnote{In keeping with the style of the rest of the book, we alternate between \enquote{formulas} and \enquote{formulae} and wish the reader best of luck with this.} + \footnote{In keeping with the style of the rest of the book, we alternate between \enquote{formulas} and \enquote{formulae} and wish the reader best of luck with this. + (Like the book, this section may contain typos and inaccuracies. These are however not intentional.)} for which the size of all equivalent LTL formulas is $\Omega\left(2^n\right)$. Markey achieves this proof by providing a formula that is in exactly this class. Besides being smaller, PLTL formulas can also be easier to write and understand, as examples below will demonstrate. diff --git a/Assignment1/specifying-properties.tex b/Assignment1/specifying-properties.tex deleted file mode 100644 index 0f84a4e..0000000 --- a/Assignment1/specifying-properties.tex +++ /dev/null @@ -1,13 +0,0 @@ -\subsubsection{Specifying Properties} -% TODO Once operator - -\camil -\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. -\end{remark} diff --git a/Assignment1/syntax.tex b/Assignment1/syntax.tex index 8543669..708d3b8 100644 --- a/Assignment1/syntax.tex +++ b/Assignment1/syntax.tex @@ -61,6 +61,7 @@ In discourse, it can be helpful to distinguish different kinds of PLTL formulas. Note that the classes \wffn, \wffp\ and \wfff\ are mutually disjoint. Furthermore, there are \wff\ which are neither, like $\Xop a \land \Xop^{-1} a$. +However, as we will see in \cref{pltl:to-ltl:syntactic}, every PLTL formula can be written as a boolean combination of $\wfff \cup \wffp \cup \wffn$. As with LTL, we can also derive additional operators in PLTL. They can be seen as counterparts of the derived LTL modalities $\square$ and $\lozenge$: @@ -70,11 +71,15 @@ They can be seen as counterparts of the derived LTL modalities $\square$ and $\l \erin \begin{definition}[Derived PLTL operators] Given $\phi \in PLTL$, then: - \begin{equation*} - \Fop^{-1} \phi \enspace\defeq\enspace \top \Sop \phi \qquad - \Gop^{-1} \phi \enspace\defeq\enspace \neg \Fop^{-1} \neg \phi + \[ + \begin{array}{rlrl} + \Fop \phi &\defeq \top \Uop \phi \qquad + & \Gop \phi &\defeq \neg \Fop \neg \phi \\ + \Fop^{-1} \phi &\defeq \top \Sop \phi + & \Gop^{-1} \phi &\defeq \neg \Fop^{-1} \neg \phi + \end{array} \qedhere - \end{equation*} + \] \end{definition} Their intuitive meaning is as follows. @@ -145,14 +150,13 @@ we include an arrow that points to the state for which the formula holds. \camil \label{pltl:dual-modalities} -Dual modalities, like the LTL $\square\lozenge$ \enquote{infinitely often} and \enquote{eventually forever}, are less useful in PLTL. +Dual modalities, like the LTL $\square\lozenge$ \enquote{infinitely often} and \enquote{eventually forever}, are less useful with past modalities. $\square^{-1}\lozenge^{-1}\phi$ intuitively holds when at every point in the past, $\phi$ held or there was a previous moment at which $\phi$ held. This is satisfied precisely when $\phi$ held at the first moment in time. Interestingly, $\lozenge^{-1}\square^{-1}\phi$ means the same: it holds when $\phi$ held from the beginning until some moment in the past. -The reason that dual modalities in PLTL are less useful is that we still consider traces with a fixed starting point. +The reason that dual past modalities are less useful is that we still consider traces with a fixed starting point. Thus, while with future modalities it is possible to look infinitely far in the future, it is not possible to look infinitely far in the past. -%TODO: Give examples of semantics along the lines of subsection 5.1.1. Before turning to the formal semantics in the next subsection, we provide some examples of PLTL formulae and their uses. \begin{example}[Properties for a Traffic Light] @@ -164,7 +168,7 @@ Before turning to the formal semantics in the next subsection, we provide some e \[\square\left(\textsl{green} \rightarrow \lnot \Pop\textsl{red}\right) \qedhere\] \end{example} -\begin{example}[Properties for an Authentication System] +\begin{example}[A property for an Authentication System] \label{ex:pltl:authentication-system} \citet{FiterauBrostean2017} use past modalities to describe properties of the Secure Shell (SSH) protocol. One property says that if a channel is opened, there must have been some successful authentication attempt in the past~\citep[p.~149]{FiterauBrostean2017}. @@ -177,4 +181,14 @@ Before turning to the formal semantics in the next subsection, we provide some e The LTL formula is derived algorithmically in \cref{ex:pltl-to-ltl:authentication}. The LTL formula is slightly larger than the PLTL formula and is slightly less understandable. \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. +\end{remark} \cbend -- cgit v1.2.3 From a0cbbca6b29a423abbc55ee7da62026c115cd8d1 Mon Sep 17 00:00:00 2001 From: Camil Staps Date: Wed, 18 Apr 2018 20:40:20 +0200 Subject: Check syntactic elimination rules --- Assignment1/conversion.tex | 55 +++++++++++++++++++++++++++------------------- 1 file changed, 33 insertions(+), 22 deletions(-) (limited to 'Assignment1') diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex index 3f4cf0f..4feb094 100644 --- a/Assignment1/conversion.tex +++ b/Assignment1/conversion.tex @@ -92,12 +92,12 @@ 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: - % TODO Verify all except 3 \begin{align*} - E_1 &= (a \wedge \neg \beta \Sop a) \wedge \neg \beta \wedge \neg (\alpha \Uop \beta)\\ - E_2 &= \neg \beta \wedge \neg \alpha \wedge (\neg \beta \wedge q \Sop a)\\ - E_3 &= a\Sop\neg\beta \wedge \neg \alpha \wedge q \wedge (q \wedge \neg\beta \Sop a) + E_1 &= \bot \Sop a\\ + E_2 &= (\beta \lor \alpha \land \alpha \Uop \beta) \land (\neg a \lor \neg c) \Sop a\\ + E_3 &= \neg(\beta \lor \alpha \land \alpha \Uop \beta) \land (\neg a \lor \neg c) \Sop a \land (\neg a \land \neg\beta) \Sop (\neg q \land \neg a) \end{align*} + where $c = (\neg a \land \neg\beta) \Sop (\neg q \land \neg a) \land \neg\alpha \land \neg\beta$. \item Suppose $E = q \Sop (a \wedge \neg (\alpha \Uop \beta))$, then $E \equiv E_1 \vee E_2 \vee E_3$ where: \begin{align*} @@ -106,43 +106,54 @@ For the proofs of the equivalences, we refer the reader to the appendix of \cite E_3 &= q \Sop (\neg \alpha \wedge \neg \beta \wedge q \wedge (\neg \beta \wedge q) \Sop a) \end{align*} - \item Suppose $E = (q \vee \neg (\alpha \Uop \beta)) \Sop a$, then $E \equiv \neg (\neg a \Sop \neg q \wedge (\alpha \Uop \beta) \wedge \neg a) \wedge \Fop^{-1} a$, + \item Suppose $E = (q \vee \neg (\alpha \Uop \beta)) \Sop a$, + then $E \equiv \neg (\neg a \Sop (\neg q \wedge (\alpha \Uop \beta) \wedge \neg a)) \wedge \Fop^{-1} a$, which can be reduced via rule 1. - \item Suppose $E = (q \vee \alpha \Uop \beta) \Sop (a \wedge \alpha \Uop \beta)$, then $E \equiv E_1 \vee (E_2 \wedge E_3)$ where: + \item Suppose $E = (q \vee \alpha \Uop \beta) \Sop (a \wedge \alpha \Uop \beta)$, then $E \equiv E_1 \lor E_2 \lor E_3$ where: \begin{align*} - E_1 &= (\alpha \Sop a) \wedge (\beta \vee (\alpha \wedge (\alpha \Uop \beta)))\\ - E_2 &= (\beta \vee \alpha \vee \neg(\neg\beta \Sop \neg q) \Sop \beta \wedge (\alpha \Sop a))\\ - E_3 &= (\beta \vee (\alpha \wedge (\alpha \Uop \beta))) \vee \neg (\neg\beta \Sop \neg q) + E_1 &= \alpha \Sop a \wedge (\beta \vee \alpha \wedge \alpha \Uop \beta)\\ + E_2 &= \beta \lor \alpha \land \alpha\Uop\beta \land \neg (\neg\alpha \land \neg\beta \land \neg\beta\Sop\neg q) \Sop (\beta \land \alpha \Sop a)\\ + E_3 &= \neg (\neg\alpha \land \neg\beta \land \neg\beta\Sop\neg q) \Sop (\beta \land \alpha \Sop a) \land (\beta \vee \alpha \wedge \alpha \Uop \beta) \land \neg (\neg\beta \Sop \neg q) \end{align*} \item Suppose $E = (q \vee \alpha \Uop \beta) \Sop (a \wedge \neg(\alpha \Uop \beta))$, then $E \equiv E_1 \vee E_2 \vee E_3$ where: \begin{align*} - E_1 &= (\neg \beta \wedge q \Sop a) \wedge \neg \beta \wedge \neg \alpha\\ - E_2 &= q \vee (\alpha \Uop \beta) \Sop \neg \beta \wedge \neg \alpha \wedge (q \vee (\alpha \Uop \beta)) \wedge (\neg \beta \wedge q \Sop a)\\ - E_3 &= (q \wedge \neg \beta \Sop a) \wedge \neg \beta \wedge \neg (\alpha \Uop \beta) + E_1 &= ((\neg \beta \wedge q) \Sop a) \wedge \neg \alpha \wedge \neg \beta\\ + E_2 &= [q \vee \alpha \Uop \beta] \Sop [\neg \alpha \wedge \neg \beta \wedge (q \vee \alpha \Uop \beta) \wedge (\neg \beta \wedge q) \Sop a]\\ + E_3 &= (q \wedge \neg \beta) \Sop a \wedge \neg \beta \wedge \neg (\alpha \Uop \beta) \end{align*} + $E_2$ has a $\Uop$ in a $\Sop$, but can be further rewritten using elimination 5. \item Suppose $E = (q \vee \neg(\alpha \Uop \beta)) \Sop (a \wedge \alpha \Uop \beta)$, then $E \equiv E_1 \vee E_2$ where: \begin{align*} - E_1 &= (q \vee \neg (\alpha \Uop \beta) \Sop \beta \wedge (q \vee \neg (\alpha \Uop \beta)) \wedge (\alpha \wedge q \Sop a))\\ - E_2 &= (\alpha \wedge q \Sop a) \wedge \alpha \wedge (\alpha \Uop \beta) + E_1 &= [q \vee \neg (\alpha \Uop \beta)] \Sop [\beta \wedge (q \vee \neg (\alpha \Uop \beta)) \wedge (\alpha \wedge q) \Sop a]\\ + E_2 &= (\alpha \wedge q) \Sop a \wedge \alpha \wedge \alpha \Uop \beta \end{align*} $E_1$ can be further reduced using eliminations 8 and 4. - \item Suppose $E = (q \vee \neg (\alpha \Uop \beta)) \Sop (a \wedge \neg (\alpha \Uop \beta))$, then $E \equiv \neg \Gop^{-1}(E_1 \vee E_2 \vee E_3)$ where: + + \item Suppose $E = (q \vee \neg (\alpha \Uop \beta)) \Sop (a \wedge \neg (\alpha \Uop \beta))$, then $E \equiv \neg (E_1 \vee E_2 \vee E_3)$ where: \begin{align*} - E_1 &= \neg a \vee \neg (\alpha \Uop \beta)\\ - E_2 &= \neg a \vee (\alpha \Uop \beta) \Sop \neg q \wedge (\alpha \Uop \beta) \wedge \neg a\\ - E_3 &= \neg a \vee (\alpha \Uop \beta) \Sop \neg q \wedge (\alpha \Uop \beta) + E_1 &= \square^{-1} (\neg a \vee \alpha \Uop \beta)\\ + E_2 &= (\neg a \vee \alpha \Uop \beta) \Sop (\neg q \wedge \alpha \Uop \beta \wedge \neg a)\\ + E_3 &= (\neg a \vee \alpha \Uop \beta) \Sop (\neg q \wedge \alpha \Uop \beta) \end{align*} - After elimination of $\Gop^{-1}$, this formula can be further eliminated, in particular using elimination 5. + \camil + Since $\sigma \vDash_i E_2$ entails $\sigma \vDash_i E_3$ for all $i\in\mathbb N$, we also have $E \equiv \neg(E_1 \lor E_3)$.\cbend% + \footnote{\cbcolor{red}\cbstart + According to \citet[p.~439]{Gabbay1989}, $E_3$ is \enquote{subsumed by} $E_2$. + Assuming the straightforward understanding of subsumption ($\phi$ subsumes $\psi$ if and only if $\textsl{Words}(\phi) \supseteq \textsl{Words}(\psi)$), this is incorrect and $E_2$ is subsumed by $E_3$ instead.\cbend} + The term\erin\ $E_3$ (and $E_2$) can be further eliminated, in particular using elimination 5. + \cbend{} \end{enumerate} +\erin Note that these rules can only be applied when a $\Uop$ is within the scope of a $\Sop$. -In order to move the $\Sop$ out of the scope of the $\Uop$, consider that $\Sop$ and $\Uop$ are symmetrical. -These equivalences also hold when the path is reversed, so similar elimination rules exist for the case that $\Sop$ occurs within the scope of $\Uop$. +In order to move an $\Sop$ out of the scope of a $\Uop$, consider that $\Sop$ and $\Uop$ are symmetrical. +The above equivalences also hold when the path is reversed, so similar elimination rules exist for the case that $\Sop$ occurs within the scope of $\Uop$. -The final step of the algorithm entails removing the parts of the formula that contains the $\Sop$-operators. +The final step of the algorithm entails removing the pure past formulas from the boolean combination. +After all, these formulas are meaningless for $\vDash_0$, since (using Gabbay's definitions) these formulas can only say things about exclusive past time. \camil \begin{example}[A property for an Authentication System] -- cgit v1.2.3 From 341ac08515644afb57aa30073a75bace2ec41a7b Mon Sep 17 00:00:00 2001 From: Camil Staps Date: Wed, 18 Apr 2018 20:40:46 +0200 Subject: (for me) more intuitive intuitive semantics --- Assignment1/syntax.tex | 27 +++++++++++++++------------ 1 file changed, 15 insertions(+), 12 deletions(-) (limited to 'Assignment1') diff --git a/Assignment1/syntax.tex b/Assignment1/syntax.tex index 708d3b8..3f3430c 100644 --- a/Assignment1/syntax.tex +++ b/Assignment1/syntax.tex @@ -105,8 +105,8 @@ we include an arrow that points to the state for which the formula holds. \node[arbitrary] (1) [right of=0] {}; \node[state,label=$b$] (2) [right of=1] {}; \node[state,label=$a$] (3) [right of=2] {}; - \node[state,label=$a$,initial below] (4) [right of=3] {}; - \node[arbitrary] (5) [right of=4] {}; + \node (4) [right of=3] {\dots}; + \node[state,label=$a$,initial below] (5) [right of=4] {}; \node (6) [right of=5] {\dots}; \path (0) edge (1)(1) edge (2)(2) edge (3)(3) edge (4)(4) edge (5)(5) edge (6); \end{tikzpicture}\\ @@ -115,9 +115,9 @@ we include an arrow that points to the state for which the formula holds. \node (0) {\dots}; \node[arbitrary] (1) [right of=0] {}; \node[arbitrary] (2) [right of=1] {}; - \node[state,label=$a$] (3) [right of=2] {}; - \node[arbitrary,initial below] (4) [right of=3] {}; - \node[arbitrary] (5) [right of=4] {}; + \node[arbitrary] (3) [right of=2] {}; + \node[state,label=$a$] (4) [right of=3] {}; + \node[arbitrary,initial below] (5) [right of=4] {}; \node (6) [right of=5] {\dots}; \path (0) edge (1)(1) edge (2)(2) edge (3)(3) edge (4)(4) edge (5)(5) edge (6); \end{tikzpicture}\\ @@ -127,24 +127,27 @@ we include an arrow that points to the state for which the formula holds. \node[arbitrary] (1) [right of=0] {}; \node[state,label=$a$] (2) [right of=1] {}; \node[arbitrary] (3) [right of=2] {}; - \node[arbitrary,initial below] (4) [right of=3] {}; - \node[arbitrary] (5) [right of=4] {}; + \node (4) [right of=3] {\dots}; + \node[arbitrary,initial below] (5) [right of=4] {}; \node (6) [right of=5] {\dots}; \path (0) edge (1)(1) edge (2)(2) edge (3)(3) edge (4)(4) edge (5)(5) edge (6); \end{tikzpicture}\\ \text{was always} & \Gop^{-1} a & \begin{tikzpicture}[intuitive semantics] - \node (0) {\dots}; + \node[state,label=$a$] (0) {}; \node[state,label=$a$] (1) [right of=0] {}; \node[state,label=$a$] (2) [right of=1] {}; - \node[state,label=$a$] (3) [right of=2] {}; - \node[state,label=$a$,initial below] (4) [right of=3] {}; - \node[arbitrary] (5) [right of=4] {}; + \node (3) [right of=2] {\dots}; + \node[state,label=$a$] (4) [right of=3] {}; + \node[state,label=$a$,initial below] (5) [right of=4] {}; \node (6) [right of=5] {\dots}; \path (0) edge (1)(1) edge (2)(2) edge (3)(3) edge (4)(4) edge (5)(5) edge (6); \end{tikzpicture} \end{array}\] - \caption{Intuitive semantics of past modalities.} + \caption{% + Intuitive semantics of past modalities. + The current state is indicated with an arrow below. + All states following the current state are arbitrary.} \label{fig:PLTL_intuitive} \end{figure} -- cgit v1.2.3 From 205e49a4c15d291a2519eedabd683341a153aa03 Mon Sep 17 00:00:00 2001 From: Camil Staps Date: Wed, 18 Apr 2018 20:50:11 +0200 Subject: Bars everywhere --- Assignment1/assignment1.tex | 10 +++++++--- Assignment1/intro.tex | 2 +- 2 files changed, 8 insertions(+), 4 deletions(-) (limited to 'Assignment1') diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex index e8e34dd..cb1b363 100644 --- a/Assignment1/assignment1.tex +++ b/Assignment1/assignment1.tex @@ -78,8 +78,10 @@ \newif\ifchangebar\changebarfalse \let\oldcbend\cbend \def\cbend{\oldcbend\changebarfalse} -\newcommand{\erin}{\ifchangebar\cbend\fi\cbcolor{yellow}\cbstart\changebartrue} -\newcommand{\camil}{\ifchangebar\cbend\fi\cbcolor{red}\cbstart\changebartrue} +\newcommand{\changechangebar}[2][2pt]{\ifchangebar\cbend\fi\cbcolor{#2}\cbstart[#1]\changebartrue} +\newcommand{\erin}{\changechangebar{yellow}} +\newcommand{\camil}{\changechangebar{red}} +\newcommand{\both}{\changechangebar[1pt]{orange}} \renewcommand*{\arraystretch}{1.3} @@ -103,6 +105,7 @@ \begin{document} +\both \maketitle \setcounter{section}{5} @@ -120,16 +123,17 @@ \input{bibliographic-notes} \input{exercises} +\both \printbibliography \section*{Contribution} %TODO: Like we are some immature group of children, we have to provide proof of contribution -\camil Erin has started writing the text. This text was then copy-edited, slightly corrected where needed and expanded by Camil. (The result was then copy-edited, slightly corrected where needed and expanded by Erin. The result was then copy-edited, slightly corrected where needed and expanded by Camil.)$^\omega$ In the above, yellow bars indicate content primarily contributed by Erin, whereas red bars indicate content primarily contributed by Camil. +Thin orange bars indicate material that cannot be attributed to either. Unfortunately, disabilities of the \textsf{changebar} package make it impossible to indicate the fine-grainedness of our redaction process. \cbend diff --git a/Assignment1/intro.tex b/Assignment1/intro.tex index 15294ee..ddbaa5a 100644 --- a/Assignment1/intro.tex +++ b/Assignment1/intro.tex @@ -1,8 +1,8 @@ +\erin \subsection{Past Modalities in LTL}\label{sec:intro} % Explain that past Modalities are not necessary for a complete logic % Explain that PLTL does make the logic more succinct (Paper 1) %TODO: Give example on what kind of things we want to express with PLTL -\erin As mentioned in Remark 5.16, LTL can be extended with \emph{past modalities}. This section discusses this extension. The combination of LTL and Past Modalities is often called \enquote{LTL-Past} or PLTL. -- cgit v1.2.3 From 25ffc622afc727baa7c5c2918ee602b98bb291a3 Mon Sep 17 00:00:00 2001 From: Camil Staps Date: Wed, 18 Apr 2018 21:48:33 +0200 Subject: Example: protocol dependencies --- Assignment1/bad-prefix.tex | 1 + Assignment1/conversion.tex | 26 +++++++++++++++++++++++++- Assignment1/exercises.tex | 1 + Assignment1/syntax.tex | 26 +++++++++++++++++++++----- 4 files changed, 48 insertions(+), 6 deletions(-) (limited to 'Assignment1') 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 -- cgit v1.2.3