Organise in different files

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