diff options
Diffstat (limited to 'Assignment1/exercises.tex')
| -rw-r--r-- | Assignment1/exercises.tex | 30 |
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. |