1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
|
\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
\label{pltl:dual-modalities}
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
|
