summaryrefslogtreecommitdiff
path: root/Assignment1/exercises.tex
diff options
context:
space:
mode:
authorCamil Staps2018-04-12 23:07:57 +0200
committerCamil Staps2018-04-12 23:07:57 +0200
commit85bdc78e7cadd8ba52d117f648253dcc1a99c83f (patch)
tree2739de2c1ceda87a1efb006985f12cbb199ecf62 /Assignment1/exercises.tex
parentCorrect section counts (diff)
Organise in different files
Diffstat (limited to 'Assignment1/exercises.tex')
-rw-r--r--Assignment1/exercises.tex142
1 files changed, 142 insertions, 0 deletions
diff --git a/Assignment1/exercises.tex b/Assignment1/exercises.tex
new file mode 100644
index 0000000..cf2a92a
--- /dev/null
+++ b/Assignment1/exercises.tex
@@ -0,0 +1,142 @@
+\subsection{Exercises}
+% 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}}
+\camil
+\begin{exercise}
+ 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.} %TODO do you agree?
+ \[\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 $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