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
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
|
\camil
\subsection{Exercises}
\emph{NB: these exercises are to be added to the current section 5.5.}
% After the exam documentclass; http://compgroups.net/comp.text.tex/-if-else-fi-in-new-environment/263869
\newif\ifshowanswers\showanswerstrue
\newenvironment{answer}%
{\ifshowanswers\par\bgroup\small\textit{Answer:}\else\setbox0\vbox\bgroup\fi}%
{\egroup}
\newcommand{\hint}[1]{\par\textit{Hint: #1}}
\begin{exercise}
For the PLTL formulas over $AP=\{a,b\}$ given below, determine whether they are \wffn, \wffp, \wfff\ or neither.
\begin{multicols}{2}
\begin{enumerate}[label=(\alph*)]
\item $\Xop a$.
\item $a \Sop b$.
\item $(\lnot (a \land b)) \land (\lnot (\lnot a \land \lnot b))$.
\item $a \Uop a$.
\item $a \land ((b \Uop a) \lor \lnot(b \Uop a))$.
\item $\bot \rightarrow (a \Uop b)$.
\end{enumerate}
\end{multicols}
\begin{answer}
(a) \wfff;
(b) \wffp;
(c) \wffn;
(d) \wfff;
(e) neither;
(f) neither.
Note that the definition of the classes is syntactic, not semantic.
\end{answer}
\end{exercise}
\begin{exercise}
\label{ex:dual-modalities}
On page~\pageref{pltl:dual-modalities}, we discussed informally why the dual modalities $\lozenge^{-1}\square^{-1}\phi$ and $\square^{-1}\lozenge^{-1}\phi$ are both equivalent to \enquote{at the first moment in time, $\phi$}.
Prove this formally, i.e.\ that for all infinite words $\sigma$ and $i\in\mathbb N$,
\[
\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.
\]
\begin{answer}
The proof follows from the two equivalences
\begin{itemize}
\def\spacearrow{\enspace\Leftrightarrow\enspace}
\item
$\sigma \vDash_i \lozenge^{-1}\square^{-1}\phi \spacearrow
\exists_{0\le j\le i}[\sigma \vDash_j \square^{-1}\phi] \spacearrow
\exists_{0\le j\le i}\forall_{0\le k\le j}[\sigma \vDash_k \phi] \spacearrow
\sigma \vDash_0 \phi$
\enspace\ and
\item
$\sigma \vDash_i \square^{-1}\lozenge^{-1}\phi \spacearrow
\forall_{0\le j\le i}[\sigma \vDash_j \lozenge^{-1}\phi] \spacearrow
\forall_{0\le j\le i}\exists_{0\le k\le j}[\sigma \vDash_k \phi] \spacearrow
\sigma \vDash_0 \phi$.
\end{itemize}
\end{answer}
\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.
Take $n\in\mathbb N$ and $AP=\{p_0,\dots,p_n\}$.
We first show that there is no polynomial-size LTL formula expressing property~\ref{ex:proof-markey:prop-agreement}.
\begin{equation}
\phi_n(\sigma) \defeq
\forall_{i,j\in\mathbb N}
\left[
\forall_{k\in[1,n]}
[(A_i\vDash p_k) \Leftrightarrow (A_j\vDash p_k)]
\rightarrow
((A_i\vDash p_0) \Leftrightarrow (A_j\vDash p_0))
\right]
\label{ex:proof-markey:prop-agreement}
\end{equation}
where $\sigma=A_0A_1A_2\dots$.
In other words, if two points on path $\sigma$ agree on $p_k$ for all $k\in[1,n]$, the points must also agree on $p_0$.
\begin{enumerate}[label=(\alph*)]
\item Find an $\mathcal O\left(2^n\right)$ LTL formula expressing property~\ref{ex:proof-markey:prop-agreement}.
\hint{if the formula can be $\mathcal O\left(2^n\right)$, what are you allowed to quantify over?}
\begin{answer}%
\footnote{Note that this is slightly different from the version in \citet[p. 4]{Markey2003}.
The limit on the leftmost $\wedge$ has $i\in[1,n]$ rather than $i\in[0,n]$ in the original paper.
We believe this to be an error, because otherwise $a_0$ is a free variable.}
\[\phi_n(\sigma) =
\bigwedge_{\substack{a_i\in\{\top,\bot\}\\i\in[0,n]}} \left[
\left(\lozenge(\bigwedge\nolimits_{i=0}^n p_i=a_i)\right)
\rightarrow
\square\left((\bigwedge\nolimits_{i=1}^n p_i=a_i) \rightarrow p_0=a_0\right)
\right]
\]
\end{answer}
\item Assume a polynomial-size LTL formula exists for property~\ref{ex:proof-markey:prop-agreement}.
What can you say of the size of a B\"uchi automaton $\mathcal A$ recognizing $\textsl{Words}(\phi_n)$?
\label{ex:proof-markey:assumption}
\hint{consider Theorem 5.41.}
\begin{answer}
There exists a B\"uchi automaton of size $\mathcal O(2^{n^k})$ for some $k\in\mathbb N$.
\end{answer}
\item Let $A=a_0,\dots,a_{2^n-1}$ be any permutation of $2^{AP\setminus\{p_0\}}$.
Define the series $w_K=b_{K,0}\dots b_{K,2^n-1}$ with
\[
b_{K,i} \defeq
\begin{cases}
a_i & \text{iff $i\notin K$}\\
a_i \cup \{p_0\} & \text{iff $i\in K$.}
\end{cases}
\]
Show that if $K,K' \subseteq \{0,\dots,2^n-1\}$ and $K\ne K'$, also $w_K \ne w_{K'}$.
\label{ex:proof-markey:different-w_K}
\begin{answer}
Without loss of generality, assume there exists an $i\in K$ with $i\notin K'$.
Then $p_0\in b_{K,i}$ but $p_0\notin b_{K',i}$.
Hence, $w_K\ne w_{K'}$.
\end{answer}
\item How many distinct words $w_K$ exist?
\label{ex:proof-markey:nr-of-w_k}
\begin{answer}
There are $2^{|\{0,\dots,2^n-1\}|} = 2^{2^n}$ distinct $K$ (and equally many distinct $w_K$).
\end{answer}
\item Show that $w_K^\omega$ is accepted by $\mathcal A$.
\begin{answer}
Since all $a_i$ are distinct,
two points $b_{K,j}, b_{K,k}$ on $w_K^\omega$ agree on all $p_i$ for $i\in[1,n]$ iff $j\equiv k \pmod{2^n}$.
In this case, they also agree on $p_0$.
\end{answer}
\item It follows that there are paths $\pi_K$ and $\pi_{K'}$ in $\mathcal A$ accepting $w_K^\omega$ and $w_{K'}^\omega$ respectively.
Let $q_K$ and $q_{K'}$ be the $2^n$-th states of each of these paths.
Assume that $q_K = q_{K'}$.
Construct from $w_K$ and $w_{K'}$ an infinite word $v$ that is accepted by $\mathcal A$ but does not satisfy $\phi_n$.
\hint{take the simplest infinite word using both words that you can think of.}
\begin{answer}
Take $v=w_Kw_{K'}^\omega$.
Apart from the prefix of size $2^n$, the path of this word is equal to that of $w_{K'}^\omega$, which is accepted.
So $v$ is accepted.
From \ref{ex:proof-markey:different-w_K} we have an $i$ such that $p_0\in b_{K,i}$ but $p_0\notin b_{K',i}$.
However, for all $i\in[1,n]$, $p_i\in b_{K,i} \Leftrightarrow p_i\in b_{K',i}$.
Therefore, $i=i, j=i+2^n$ is a counterexample to the outermost quantifier of $\phi_n$.
\end{answer}
\item Show that this contradicts the assumption from \ref{ex:proof-markey:assumption}.
\begin{answer}
Since we have $2^{2^n}$ distinct $w_K$ [cf. \ref{ex:proof-markey:nr-of-w_k}] and the $2^n$-th states of their accepting paths must all be distinct,
$\mathcal A$ has at least $2^{2^n}$ states.
But $2^{2^n} \notin \mathcal O(2^{n^k})$.
\end{answer}
\item We now turn to a slightly different property:
\begin{equation}
\psi_n(\sigma) \defeq
\forall_{i\in\mathbb N}
\left[
\forall_{k\in[1,n]}
[(A_i\vDash p_k) \Leftrightarrow (A_0\vDash p_k)]
\rightarrow
((A_i\vDash p_0) \Leftrightarrow (A_0\vDash p_0))
\right]
\label{ex:proof-markey:prop-agreement-2}
\end{equation}
Property \ref{ex:proof-markey:prop-agreement-2} holds if all points on $\sigma$ that agree with all $p_k$ for $k\in[1,n]$ with $A_n$ also agree on $p_0$.
Give an $\mathcal O(n)$ PLTL formula expressing property \ref{ex:proof-markey:prop-agreement-2}.
\hint{recall the semantics of the dual modalities in PLTL.}
\begin{answer}
\[\psi_n(\sigma) =
\square\left[
\left(\bigwedge\nolimits_{i=1}^n (p_i \Leftrightarrow \lozenge^{-1}\square^{-1}p_i)\right)
\Rightarrow
(p_0 \Leftrightarrow \lozenge^{-1}\square^{-1}p_0)
\right]
\]
\end{answer}
\item Construct an LTL formula for $\phi_n$ using the PLTL formula for $\psi_n$ and conclude the proof.
\hint{first construct an LTL formula for $\psi_n$.}
\begin{answer}
Take $\phi'_n \defeq \square\psi'_n$, where $\psi'_n$ is an LTL formula initially equivalent to $\psi_n$.
By virtue of the $\square$ operator, $\phi_n\equiv\phi'_n$.
But $\phi_n$ is $\mathcal O(2^n$, so also $\phi'_n$ is exponential.
Since $\phi'_n$ is $\mathcal O(2^n)$ and $\psi_n$ is $\mathcal O(n)$,
the PLTL formula for property~\ref{ex:proof-markey:prop-agreement-2} is exponentially more succinct than the LTL formula.
\qed
\end{answer}
\end{enumerate}
\end{exercise}
\cbend
|
