Add an exercise based on Markey's proof; extend the grammar because we allow PLTL formulas inside LTL formulas

1 files changed, 183 insertions, 27 deletions

diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex
index 0149906..610f7ec 100644
--- a/Assignment1/assignment1.tex
+++ b/Assignment1/assignment1.tex
@@ -6,6 +6,7 @@
 \usepackage{amsmath}
 \usepackage{amsthm}
 \usepackage{amssymb}
+\renewcommand{\qedsymbol}{$\blacksquare$}
 \let\leq\leqslant
 \let\le\leqslant
 % See http://www.ams.org/faq?faq_id=212 for the trick to add qed at the end of
@@ -21,7 +22,7 @@
 \theoremstyle{mydefinition}
 \newtheorem{xdefinition}{Definition}
 \newenvironment{definition}%
-	{\renewcommand{\qedsymbol}{$\blacksquare$}\pushQED{\qed}\begin{xdefinition}}%
+	{\pushQED{\qed}\begin{xdefinition}}%
 	{\popQED\end{xdefinition}}
 \newtheoremstyle{myexample}%
 	{2em}{2em}% Space above and below
@@ -34,12 +35,15 @@
 \theoremstyle{myexample}
 \newtheorem{xexample}{Example}
 \newenvironment{example}%
-	{\renewcommand{\qedsymbol}{$\blacksquare$}\pushQED{\qed}\begin{xexample}}%
+	{\pushQED{\qed}\begin{xexample}}%
 	{\popQED\end{xexample}}
 \newtheorem{xremark}{Remark}
 \newenvironment{remark}%
-	{\renewcommand{\qedsymbol}{$\blacksquare$}\pushQED{\qed}\begin{xremark}}%
+	{\pushQED{\qed}\begin{xremark}}%
 	{\popQED\end{xremark}}
+\newtheoremstyle{exercise}{1em}{1em}{}{}{\scshape}{.}{1em}{}
+\theoremstyle{exercise}
+\newtheorem{exercise}{Exercise}
 \usepackage{mathtools}
 \usepackage{mdframed}
 \usepackage{tikz}
@@ -47,6 +51,7 @@
 \usepackage{relsize}
 \usepackage{parskip}
 \usepackage{cleveref}
+\usepackage{enumitem}
 \usepackage{stackengine}
 \crefname{figure}{Figure}{Figures}
 \usepackage[color]{changebar}
@@ -106,14 +111,8 @@ For this reason, it is useful to discuss them here.
 % Provide intuitive semantics
 %TODO: Provide formal semantics
 \erin
-This subsection describes the syntax and semantics of PLTL.%
-\footnote{%
-	Given that PLTL is an extension of LTL, we are left with two options.
-	The first option is to define the entire syntax of PLTL without considering that we have already defined LTL.
-	This option is slightly more verbose, but does not depend on subsection 5.1.1.
-	The second option, which we will adopt here, builds on the syntax and semantics that are already defined for LTL formulae.}
-All LTL formulae are PLTL formulae.
-Two additional operators are added:
+This subsection describes the syntax of PLTL.
+PLTL uses the same operators as LTL and adds two additional operators:
 	$\Pop$ (pronounced \enquote{previously}) and
 	$\Sop$ (pronounced \enquote{since}).
 The $\Pop$-modality is comparable to $\Xop$.
@@ -122,17 +121,25 @@ The $\Sop$-modality is comparable to $\Uop$: $\phi_1\Sop\phi_2$ holds if $\phi_2
 	and $\phi_1$ held ever after that moment up to and including the current moment.
 
 \begin{definition}[Syntax of PLTL]
-	PLTL formulae over the set $LTL$ of LTL formulae are formed according to the following grammar:
-	$$
-		\phi ::= l
-		\mid \Pop \phi
-		\mid \phi_1 \Sop \phi_2
-	$$
-	where $l \in LTL$.
+	PLTL formulae over the set $AP$ of atomic propositions are formed according to the following grammar:
+	\[
+		\phi
+			::=
+			\left.\raisebox{0pt}[5pt][5pt]{} \text{true}
+			\enspace\middle|\enspace a
+			\enspace\middle|\enspace \phi_1 \land \phi_2
+			\enspace\middle|\enspace \lnot \phi
+			\enspace\middle|\enspace \bigcirc \phi
+			\enspace\middle|\enspace \phi_1 \Uop \phi_2
+			\enspace\middle|\enspace \Pop \phi
+			\enspace\middle|\enspace \phi_1 \Sop \phi_2
+			\right.
+	\]
+	where $a \in AP$.
 \end{definition}
 
 \camil
-The precedence order of the LTL operators remains the same.
+The precedence order of the operators borrowed from LTL remains the same.
 $\Pop$ binds equally strong as $\Xop$ and $\lnot$.
 $\Sop$ takes precedence over $\Uop$, and like $\Uop$ is right-associative.
 
@@ -273,16 +280,22 @@ We use $\sigma \vDash \phi$ as a shorthand for $\sigma \vDash_0 \phi$.
 \erin
 \begin{definition}[Semantics of PLTL (Interpretation over Words)]
 	Let $\phi$ be a PLTL formula over $AP$. The LT property induced by $\phi$ is
-	$$Words(\phi) = \{\sigma \in \left(2^{AP}\right)^\omega \mid \sigma \vDash \phi\}$$
+	\[Words(\phi) = \{\sigma \in \left(2^{AP}\right)^\omega \mid \sigma \vDash \phi\}\]
 	where $\vDash\ \subseteq \left(2^{AP}\right)^\omega \times \mathbb{N} \times PLTL$ is the smallest relation with the properties in \cref{fig:PLTL-semantics}.
 \end{definition}
 \camil
 Note that we must redefine the satisfaction relation for the LTL operators, because $\vDash$ is now a ternary relation.
+The difference with LTL formulae is well illustrated by the $\bigcirc$ operator.
+In the LTL case, $\sigma=A_0A_1A_2\dots\vDash\bigcirc\phi$ iff $\sigma[1\dots]=A_1A_2\dots\vDash\phi$.
+Thus, whether $\bigcirc\phi$ holds for $\sigma$ cannot depend on $A_0$.
+In the PLTL case, $\sigma\vDash_i\bigcirc\phi$ iff $\sigma\vDash_{i+1}\phi$.
+The information about $A_0$ is not lost, so whether $\bigcirc\phi$ holds for $\sigma$ may depend on $A_0$,
+	as is trivially the case with $\bigcirc\bigcirc^{-1}a$.
 
 \begin{figure}
 	\centering
 	\begin{mdframed}
-	$$
+	\[
 		\begin{matrix*}[l]
 			\sigma &\vDash_i & \text{true}\\
 			\sigma &\vDash_i & a                 &\text{iff} & a\in A_i\\
@@ -293,7 +306,7 @@ Note that we must redefine the satisfaction relation for the LTL operators, beca
 			\sigma &\vDash_i & \phi_1\Sop\phi_2  &\text{iff} & \exists_{j \le i}.\text{$\sigma \vDash_j \phi_2$ and $\sigma \vDash_k \phi_1$ for all $j < k \le i$}\\
 			\sigma &\vDash_i & \Pop\phi          &\text{iff} & i \geq 1 \wedge \sigma \vDash_{i-1} \phi
 		\end{matrix*}
-	$$
+	\]
 	\end{mdframed}
 	\caption{PLTL semantics for infinite words $\sigma=A_0A_1A_2\dots \in \left(2^{AP}\right)^\omega$.}
 	\label{fig:PLTL-semantics}
@@ -304,9 +317,9 @@ Note that we must redefine the satisfaction relation for the LTL operators, beca
 	Let $TS = (S, Act, \rightarrow, I, AP, L)$ be a transition system without terminal states, and let $\phi$ be an PLTL-formula over AP.
 	\begin{itemize}
 		\item For infinite path fragments $\pi$ of $TS$, the satisfaction relation is defined by
-			$$\pi \vDash \phi \Leftrightarrow trace(\pi) \vDash \phi$$
+			\[\pi \vDash \phi \Leftrightarrow trace(\pi) \vDash \phi\]
 		\item For state $s \in S$, the satisfaction relation $\vDash$ is defined by
-			$$s \vDash \phi \Leftrightarrow \forall_{\pi \in Paths(s)}[\pi \vDash \phi]$$
+			\[s \vDash \phi \Leftrightarrow \forall_{\pi \in Paths(s)}[\pi \vDash \phi]\]
 			\item $TS$ satisfies $\phi$, denoted by $TS \vDash \phi$ if $Traces \vDash \phi$, if $Traces(TS) \subseteq Words(\phi)$
 				\qedhere
 	\end{itemize}
@@ -317,12 +330,12 @@ we must provide their semantics.
 Note that we need to add a index $i$, since we must also be able to look in the past.
 
 Given these definitions, it is possible to derive the formal semantics of the $\Fop^{-1}$ and $\Gop^{-1}$ operators as well:
-$$
+\[
 	\begin{matrix*}[l]
 		\sigma &\vDash_i &\Fop^{-1}\phi &\text{iff} &\exists_{k \leq i}[\sigma \vDash_k \phi]\\
 		\sigma &\vDash_i &\Gop^{-1}\phi &\text{iff} &\forall_{k \leq i}[\sigma \vDash_k \phi]
 	\end{matrix*}
-$$
+\]
 
 \subsubsection{Specifying Properties}
 % TODO Once operator
@@ -350,7 +363,7 @@ we can define equivalence on PLTL formulas.
 
 Additionally, we can define another form of equivalence, initial equivalence:
 \begin{definition}[Initial Equivalence of PLTL Formulae]
-	PLTL formulae $\phi_1,\phi_2$ are initial equivalent, denoted $\phi_1 \equiv_0 \phi_2$ iff they verify the following property:
+	PLTL formulae $\phi_1,\phi_2$ are initially equivalent, denoted $\phi_1 \equiv_0 \phi_2$ iff they verify the following property:
 	\[\text{for any path } \pi, \pi \vDash_0 \phi \Leftrightarrow \pi \vDash_0 \psi \qedhere\]
 \end{definition}
 \cbend
@@ -376,6 +389,149 @@ Additionally, we can define another form of equivalence, initial equivalence:
 % A possibly helpful list is at https://cstheory.stackexchange.com/a/29452
 % Also the bibliography file should be worked through.
 
+\section{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
+
 \section{Contribution}
 %TODO: Like we are some immature group of children, we have to provide proof of contribution
 \camil