\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