diff options
Diffstat (limited to 'Assignment1/syntax.tex')
| -rw-r--r-- | Assignment1/syntax.tex | 153 |
1 files changed, 153 insertions, 0 deletions
diff --git a/Assignment1/syntax.tex b/Assignment1/syntax.tex new file mode 100644 index 0000000..babf688 --- /dev/null +++ b/Assignment1/syntax.tex @@ -0,0 +1,153 @@ +\subsubsection{Syntax} +% Provide formal syntax +% Provide intuitive semantics +%TODO: Provide formal semantics +\erin +This subsection describes the syntax of PLTL. +PLTL uses the same operators as LTL and adds two additional operators: + $\Pop$ (pronounced \enquote{previously}) and + $\Sop$ (pronounced \enquote{since}). +The $\Pop$-modality is comparable to $\Xop$. +Formula $\Pop\phi$ holds at some moment if $\phi$ held in the previous \enquote{step}. +The $\Sop$-modality is comparable to $\Uop$: $\phi_1\Sop\phi_2$ holds if $\phi_2$ held at some previous moment + and $\phi_1$ held ever after that moment up to and including the current moment. + +\begin{definition}[Syntax of PLTL] + PLTL formulae over the set $AP$ of atomic propositions are formed according to the following grammar: + \[ + \phi + ::= + \left.\raisebox{0pt}[5pt][5pt]{} \text{true} + \enspace\middle|\enspace a + \enspace\middle|\enspace \phi_1 \land \phi_2 + \enspace\middle|\enspace \lnot \phi + \enspace\middle|\enspace \bigcirc \phi + \enspace\middle|\enspace \phi_1 \Uop \phi_2 + \enspace\middle|\enspace \Pop \phi + \enspace\middle|\enspace \phi_1 \Sop \phi_2 + \right. + \] + where $a \in AP$. +\end{definition} + +\camil +The precedence order of the operators borrowed from LTL remains the same. +$\Pop$ binds equally strong as $\Xop$ and $\lnot$. +$\Sop$ takes precedence over $\Uop$, and like $\Uop$ is right-associative. + +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$: + $\square^{-1}$ (\enquote{was always}, since the beginning until now) and + $\lozenge^{-1}$ (\enquote{was sometime}, now or at some point before now). + +\erin +\begin{definition}[Derived PLTL operators] + Given $\phi \in PLTL$, then: + \begin{equation*} + \Fop^{-1} \phi \defeq \top \Sop \phi \qquad + \Gop^{-1} \phi \defeq \neg \Fop^{-1} \neg \phi + \qedhere + \end{equation*} +\end{definition} + +Their intuitive meaning is as follows. +$\Fop^{-1} \phi$ ensures that at some point in the past $\phi$ was true. +$\Gop^{-1} \phi$ is satisfied when there is no moment in the past on which $\phi$ did not hold. +In other words, $\Gop^{-1}$ entails that $\phi$ held globally until this point. + +\Cref{fig:PLTL_intuitive} shows the intuitive meanings of the past modalities for the simple case where $a$ and $b$ are the only atomic propositions. +The left hand side of the figure shows some PLTL formulae; +the right hand side shows sequences for which this formula holds. +Since we need to also consider the past, +we include an arrow that points to the state for which the formula holds. + +\begin{figure} + \tikzset{intuitive semantics/.style={shorten >=1pt,node distance=16mm,on grid,initial text={},baseline=-0.5ex,->}} + \tikzset{state/.append style={minimum size=15pt}} + \tikzset{arbitrary/.style={state,label={[font=\relsize{-2}]arbitrary}}} + \centering + \[\begin{array}{rcl} + \text{since} & a \Sop b & + \begin{tikzpicture}[intuitive semantics] + \node (0) {\dots}; + \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 (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{previously} & \Pop a & + \begin{tikzpicture}[intuitive semantics] + \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 (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 sometime} & \Fop^{-1} a & + \begin{tikzpicture}[intuitive semantics] + \node (0) {\dots}; + \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 (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$] (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 (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.} + \label{fig:PLTL_intuitive} +\end{figure} + +\camil +Dual modalities, like the LTL $\square\lozenge$ \enquote{infinitely often} and \enquote{eventually forever}, are less useful in PLTL. +$\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. +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. + +\begin{example}[Properties for a Traffic Light] + We return to the traffic light of Example 5.4. + Since dual past modalities are less useful than dual future modalities, we cannot express the liveness property $\square\lozenge\textsl{green}$ with a pure past formula. + However, the requirement \enquote{once red, the light cannot become green immediately} \emph{can} be expressed with past modalities. + To rewrite it, consider that this requirements is equivalent to \enquote{if green, the light cannot have been red previously}. + This yields the formula: + \[\square\left(\textsl{green} \rightarrow \lnot \Pop\textsl{red}\right) \qedhere\] +\end{example} + +\begin{example}[Properties for an 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*} +\end{example} +\cbend |