\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