diff options
| -rw-r--r-- | Assignment1/assignment1.tex | 2 | ||||
| -rw-r--r-- | Assignment1/exercises.tex | 30 | ||||
| -rw-r--r-- | Assignment1/semantics.tex | 10 | ||||
| -rw-r--r-- | Assignment1/syntax.tex | 1 |
4 files changed, 38 insertions, 5 deletions
diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex index 027142a..3c9d766 100644 --- a/Assignment1/assignment1.tex +++ b/Assignment1/assignment1.tex @@ -9,6 +9,8 @@ \renewcommand{\qedsymbol}{$\blacksquare$} \let\leq\leqslant \let\le\leqslant +\let\geq\geqslant +\let\ge\geqslant % See http://www.ams.org/faq?faq_id=212 for the trick to add qed at the end of % definitions and examples. \newtheoremstyle{mydefinition}% 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. diff --git a/Assignment1/semantics.tex b/Assignment1/semantics.tex index 43942b5..f851b14 100644 --- a/Assignment1/semantics.tex +++ b/Assignment1/semantics.tex @@ -40,9 +40,9 @@ The information about $A_0$ is not lost, so whether $\bigcirc\phi$ holds for $\s \sigma &\vDash_i & \phi_1\land\phi_2 &\text{iff} & \text{$\sigma\vDash_i\phi_1$ and $\sigma\vDash_i\phi_2$}\\ \sigma &\vDash_i & \lnot\phi &\text{iff} & \sigma \nvDash_i \phi\\ \sigma &\vDash_i & \bigcirc\phi &\text{iff} & \sigma \vDash_{i+1} \phi\\ - \sigma &\vDash_i & \phi_1\Uop\phi_2 &\text{iff} & \exists_{j \le 0}.\text{$\sigma \vDash_j \phi_2$ and $\sigma \vDash_i \phi_1$ for all $0 \le i < j$}\\ - \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 + \sigma &\vDash_i & \phi_1\Uop\phi_2 &\text{iff} & \exists_{j \ge 0}.\text{$\sigma \vDash_j \phi_2$ and $\sigma \vDash_i \phi_1$ for all $0 \le i < j$}\\ + \sigma &\vDash_i & \phi_1\Sop\phi_2 &\text{iff} & \exists_{0 \le 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} & \text{$i \geq 1$ and $\sigma \vDash_{i-1} \phi$} \end{matrix*} \] \end{mdframed} @@ -70,7 +70,7 @@ Note that we need to add a index $i$, since we must also be able to look in the 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] + \sigma &\vDash_i &\Fop^{-1}\phi &\text{iff} &\exists_{0 \leq k \leq i}[\sigma \vDash_k \phi]\\ + \sigma &\vDash_i &\Gop^{-1}\phi &\text{iff} &\forall_{0 \leq k \leq i}[\sigma \vDash_k \phi] \end{matrix*} \] diff --git a/Assignment1/syntax.tex b/Assignment1/syntax.tex index babf688..6fc0002 100644 --- a/Assignment1/syntax.tex +++ b/Assignment1/syntax.tex @@ -117,6 +117,7 @@ we include an arrow that points to the state for which the formula holds. \end{figure} \camil +\label{pltl:dual-modalities} Dual modalities, like the LTL $\square\lozenge$ \enquote{infinitely often} and \enquote{eventually forever}, are less useful in PLTL. $\square^{-1}\lozenge^{-1}\phi$ intuitively holds when at every point in the past, $\phi$ held or there was a previous moment at which $\phi$ held. This is satisfied precisely when $\phi$ held at the first moment in time. |