diff options
author | Camil Staps | 2018-04-12 23:07:57 +0200 |
---|---|---|
committer | Camil Staps | 2018-04-12 23:07:57 +0200 |
commit | 85bdc78e7cadd8ba52d117f648253dcc1a99c83f (patch) | |
tree | 2739de2c1ceda87a1efb006985f12cbb199ecf62 /Assignment1/exercises.tex | |
parent | Correct section counts (diff) |
Organise in different files
Diffstat (limited to 'Assignment1/exercises.tex')
-rw-r--r-- | Assignment1/exercises.tex | 142 |
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 |