Add an exercise about dual modalities

1 files changed, 30 insertions, 0 deletions

diff --git a/Assignment1/exercises.tex b/Assignment1/exercises.tex
index cf2a92a..371dc0f 100644
--- a/Assignment1/exercises.tex
+++ b/Assignment1/exercises.tex
@@ -5,8 +5,38 @@
 	{\ifshowanswers\par\bgroup\small\textit{Answer:}\else\setbox0\vbox\bgroup\fi}%
 	{\egroup}
 \newcommand{\hint}[1]{\par\textit{Hint: #1}}
+
 \camil
 \begin{exercise}
+	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}
 	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.