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
|
\erin
\subsubsection{Semantics}
The semantics of LTL and PLTL are defined in a very similar way.
However, we must make some modifications to the definitions.
\camil
In particular, the $\vDash$ operator must be redefined.
Recall that for LTL we wrote $\sigma \vDash \phi$ when $\sigma$ satisfies $\phi$ and $\sigma[i\dots]$ for the suffix of $\sigma$ starting in the $(j+1)$st symbol.
The latter notation effectively loses information about the prefix.
In the case of PLTL, we cannot lose this information.
For this reason, we use a satisfaction relation at a specific index.
We will write this as $\sigma \vDash_i \phi$, read as \enquote{$\sigma$ satisfies $\phi$ at $i$}.%
\footnote{%
The notation used in literature varies.
\citet{Lichtenstein1985} use $(\sigma,i) \vDash \phi$; \citet{Markey2003} uses $\sigma,i \vDash \phi$.
Although the difference is minor, we find $\vDash_i$ more intuitive because it shows that the object being checked is the same in $\sigma\vDash_i\phi$ and $\sigma\vDash_j\phi$.}
We use $\sigma \vDash \phi$ as a shorthand for $\sigma \vDash_0 \phi$.
\erin
\begin{definition}[Semantics of PLTL (Interpretation over Words)]
\label{def:pltl:semantics-words}
Let $\phi$ be a PLTL formula over $AP$. The LT property induced by $\phi$ is
\[Words(\phi) = \{\sigma \in \left(2^{AP}\right)^\omega \mid \sigma \vDash \phi\}\]
where $\vDash\ \subseteq \left(2^{AP}\right)^\omega \times \mathbb{N} \times PLTL$ is the smallest relation with the properties in \cref{fig:PLTL-semantics}.
\end{definition}
\camil
Note that we must redefine the satisfaction relation for the LTL operators, because $\vDash$ is now a ternary relation.
The difference with LTL formulae is well illustrated by the $\Xop$ operator.
In the LTL case, $\sigma=A_0A_1A_2\dots\vDash\Xop\phi$ iff $\sigma[1\dots]=A_1A_2\dots\vDash\phi$.
Thus, whether $\Xop\phi$ holds for $\sigma$ cannot depend on $A_0$.
In the PLTL case, $\sigma\vDash_i\Xop\phi$ iff $\sigma\vDash_{i+1}\phi$.
The information about $A_0$ is not lost, so whether $\Xop\phi$ holds for $\sigma$ may depend on $A_0$,
as is trivially the case with $\Xop\Xop^{-1}a$.
\begin{figure}
\centering
\begin{mdframed}
\[
\begin{matrix*}[l]
\sigma &\vDash_i & \top\\
\sigma &\vDash_i & a &\text{iff} & a\in A_i\\
\sigma &\vDash_i & \phi_1\land\phi_2 &\text{iff} & \text{$\sigma\vDash_i\phi_1$ and $\sigma\vDash_i\phi_2$}\\
\sigma &\vDash_i & \lnot\phi &\text{iff} & \sigma \nvDash_i \phi\\
\sigma &\vDash_i & \Xop\phi &\text{iff} & \sigma \vDash_{i+1} \phi\\
\sigma &\vDash_i & \phi_1\Uop\phi_2 &\text{iff} & \exists_{j \ge i}\big[\text{$\sigma \vDash_j \phi_2$ and $\sigma \vDash_k \phi_1$ for all $i \le k < j$}\big]\\
\sigma &\vDash_i & \phi_1\Sop\phi_2 &\text{iff} & \exists_{0 \le j \le i}\big[\text{$\sigma \vDash_j \phi_2$ and $\sigma \vDash_k \phi_1$ for all $j < k \le i$}\big]\\
\sigma &\vDash_i & \Pop\phi &\text{iff} & \text{$i \geq 1$ and $\sigma \vDash_{i-1} \phi$}
\end{matrix*}
\]
\end{mdframed}
\caption{PLTL semantics for infinite words $\sigma=A_0A_1A_2\dots \in \left(2^{AP}\right)^\omega$.}
\label{fig:PLTL-semantics}
\end{figure}
\begin{example}[Satisfaction of PLTL Formulae by Words]
Let $\pi = aabcdcdcd\dots$ be an infinite path over $AP=\{a,b,c,d\}$, of which on every moment only one atomic proposition holds (i.e., at position 0, $a$ holds, at position 2, $b$ holds, etc.).
We have for instance:
\begin{itemize}
\item For all $i\in\mathbb N$, $\pi \vDash_i b \rightarrow \Xop^{-1}a$.
If $i \ne 2$, $b$ does not hold and the implication is trivially satisfied.
If $i = 2$, we have $\pi \vDash_{i-1} a$ and the formula is satisfied as well.
\item For all $i\ge 2$, $\pi \vDash_i (d \rightarrow \Xop^{-1} c) \Sop b$.
We need to give $0 \le j \le i$ with $\pi \vDash_j b$ and $\pi \vDash_k d \rightarrow \Xop^{-1} c$ for all $j < k \le i$.
Clearly, we can only give $j=2$.
Then for odd positions $k$, the implication $d \rightarrow \Xop^{-1} c$ holds trivially since $d$ does not hold.
For even positions $k$, it holds as well since $c$ holds at odd positions $n > 2$.
\qedhere
\end{itemize}
\end{example}
\erin
Given these definitions, it is possible to derive the formal semantics of the $\Fop^{-1}$ and $\Gop^{-1}$ operators as well:
\[
\begin{matrix*}[l]
\sigma &\vDash_i &\Fop^{-1}\phi &\text{iff} &\exists_{0 \leq j \leq i}[\sigma \vDash_j \phi]\\
\sigma &\vDash_i &\Gop^{-1}\phi &\text{iff} &\forall_{0 \leq j \leq i}[\sigma \vDash_j \phi]
\end{matrix*}
\]
\camil
The first follows from the rule for $\Sop$ and the fact that $\sigma \vDash_i \top$ for all $i\in\mathbb N$.
The second follows from:
\begin{align*}
\sigma \vDash_i \square^{-1}\phi
&\quad\Leftrightarrow\quad \sigma \vDash_i \lnot\lozenge^{-1}\lnot\phi\\
&\quad\Leftrightarrow\quad \sigma \nvDash_i \lozenge^{-1}\lnot\phi\\
&\quad\Leftrightarrow\quad \nexists_{0\le j\le i} [\sigma \vDash_j \lnot\phi]\\
&\quad\Leftrightarrow\quad \forall_{0\le j\le i} [\sigma \vDash_j \phi].
\end{align*}
With this result we can also derive the semantics of the dual modalities $\lozenge^{-1}\square^{-1}$ and $\square^{-1}\lozenge^{-1}$:
\[
\sigma \vDash_i \lozenge^{-1}\square^{-1}\phi
\quad\Leftrightarrow\quad
\sigma \vDash_i \square^{-1}\lozenge^{-1}\phi
\quad\Leftrightarrow\quad
\sigma \vDash_0 \phi
\]
This is done in \cref{ex:dual-modalities}.
The semantics over words extend to transition systems similar to the LTL case in Definition 5.7.
The only difference is that $\vDash$ now is a ternary relation, and we use $\pi\vDash\phi$ as a shorthand for $\pi\vDash_0\phi$.
\begin{figure}[ht]
\centering
\begin{tikzpicture}[initial text={},node distance=3cm,->]
\node[state,label=below:{$\{a,b\}$},initial] (s1) {$s_1$};
\node[state,label=below:{$\{a,b\}$},right of=s1] (s2) {$s_2$};
\node[state,label=below:{$\{a\}$},right of=s2,initial right] (s3) {$s_3$};
\draw (s1) edge[bend left] (s2);
\draw (s2) edge[bend left] (s1);
\draw (s2) -- (s3);
\draw (s3) edge[loop above,looseness=8,in=60,out=120] (s3);
\end{tikzpicture}
\caption{Example for semantics of PLTL.}
\label{fig:pltl:example-ts}
\end{figure}
\begin{example}[Satisfaction of PLTL Formulae by Transition Systems]
Consider again the transition system $TS$ from Figure 5.3, reproduced as \cref{fig:pltl:example-ts}.
\begin{itemize}
\item
Recall that $TS \vDash \square a$.
A noteworthy peculiarity is that $TS \nvDash \square\Xop^{-1}a$, since $\Xop^{-1}\phi$ is always false at position 0.
Clearly, we do have $TS \vDash_i \square\Xop^{-1}a$ for $i \ge 1$.
\item
We also have $TS \vDash \square(b \rightarrow \square^{-1}b)$.
After all, if $b$ does not hold, $b$ will never hold again.
\item
We have $s_1 \vDash \square(a \Sop b)$:
since $a$ always holds, this is for $TS$ equivalent to $\square(\top \Sop b) \equiv \square(\lozenge^{-1}b)$, and $s_1 \vDash b$.
However, since $s_2 \nvDash \square(a \Sop b)$ (because $a^\omega \nvDash \square(a \Sop b)$), also $TS \nvDash \square(a \Sop b)$.
\qedhere
\end{itemize}
\end{example}
\cbend
|
