diff options
Diffstat (limited to 'Assignment1/syntax.tex')
| -rw-r--r-- | Assignment1/syntax.tex | 87 |
1 files changed, 59 insertions, 28 deletions
diff --git a/Assignment1/syntax.tex b/Assignment1/syntax.tex index 6571564..81a7d7f 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. @@ -100,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}\\ @@ -110,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}\\ @@ -122,37 +127,39 @@ 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} \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,19 +171,43 @@ 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}. 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} + +\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] + Like for LTL, many different notations are used in literature for PLTL. + These include + $\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 |