diff options
| -rw-r--r-- | Assignment1/assignment1.tex | 1 | ||||
| -rw-r--r-- | Assignment1/exercises.tex | 3 | ||||
| -rw-r--r-- | Assignment1/semantics.tex | 40 | ||||
| -rw-r--r-- | Assignment1/syntax.tex | 10 |
4 files changed, 39 insertions, 15 deletions
diff --git a/Assignment1/assignment1.tex b/Assignment1/assignment1.tex index e40b064..63645f1 100644 --- a/Assignment1/assignment1.tex +++ b/Assignment1/assignment1.tex @@ -60,6 +60,7 @@ \crefname{xdefinition}{Definition}{Definitions} \crefname{xexample}{Example}{Examples} \crefname{xremark}{Remark}{Remarks} +\crefname{exercise}{Exercise}{Exercises} \usepackage[color]{changebar} \newif\ifchangebar\changebarfalse \let\oldcbend\cbend diff --git a/Assignment1/exercises.tex b/Assignment1/exercises.tex index 9126427..5849c84 100644 --- a/Assignment1/exercises.tex +++ b/Assignment1/exercises.tex @@ -17,7 +17,7 @@ \item $(\lnot (a \land b)) \land (\lnot (\lnot a \land \lnot b))$. \item $a \Uop a$. \item $a \land ((b \Uop a) \lor \lnot(b \Uop a))$. - \item $\text{false} \rightarrow (a \Uop b)$. + \item $\bot \rightarrow (a \Uop b)$. \end{enumerate} \end{multicols} @@ -33,6 +33,7 @@ \end{exercise} \begin{exercise} + \label{ex:dual-modalities} 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$, \[ diff --git a/Assignment1/semantics.tex b/Assignment1/semantics.tex index f851b14..791eb15 100644 --- a/Assignment1/semantics.tex +++ b/Assignment1/semantics.tex @@ -35,7 +35,7 @@ The information about $A_0$ is not lost, so whether $\bigcirc\phi$ holds for $\s \begin{mdframed} \[ \begin{matrix*}[l] - \sigma &\vDash_i & \text{true}\\ + \sigma &\vDash_i & \top\\ \sigma &\vDash_i & a &\text{iff} & a\in A_i\\ \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\\ @@ -51,6 +51,35 @@ The information about $A_0$ is not lost, so whether $\bigcirc\phi$ holds for $\s \end{figure} \erin +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_{0 \leq j \leq i}[\sigma \vDash_j \phi]\\ + \sigma &\vDash_i &\Gop^{-1}\phi &\text{iff} &\forall_{0 \leq j \leq i}[\sigma \vDash_j \phi] + \end{matrix*} +\] +\camil +The first follows from the rule for $\Sop$ and the fact that $\sigma \vDash_i \top$ for all $i\in\mathbb N$. +The second follows from: +\begin{align*} + \sigma \vDash_i \square^{-1}\phi + &\quad\Leftrightarrow\quad \sigma \vDash_i \lnot\lozenge^{-1}\lnot\phi\\ + &\quad\Leftrightarrow\quad \sigma \nvDash_i \lozenge^{-1}\lnot\phi\\ + &\quad\Leftrightarrow\quad \nexists_{0\le j\le i} [\sigma \vDash_j \lnot\phi]\\ + &\quad\Leftrightarrow\quad \forall_{0\le j\le i} [\sigma \vDash_j \phi]. +\end{align*} + +With this result we can also derive the semantics of the dual modalities $\lozenge^{-1}\square^{-1}$ and $\square^{-1}\lozenge^{-1}$: +\[ + \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 +\] +This is done in \cref{ex:dual-modalities}. + +\erin \begin{definition}[Semantics of PLTL over Paths and States] 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} @@ -66,11 +95,4 @@ In order to make these definitions suitable for use with our PLTL operators, we must provide their semantics. \Cref{fig:PLTL-semantics} shows the formal semantics of the operators defined in the grammar. 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_{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*} -\] +\cbend diff --git a/Assignment1/syntax.tex b/Assignment1/syntax.tex index 833144b..81c1844 100644 --- a/Assignment1/syntax.tex +++ b/Assignment1/syntax.tex @@ -18,7 +18,7 @@ The $\Sop$-modality is comparable to $\Uop$: $\phi_1\Sop\phi_2$ holds if $\phi_2 \[ \phi ::= - \left.\raisebox{0pt}[5pt][5pt]{} \text{true} + \left.\raisebox{0pt}[5pt][5pt]{} \top \enspace\middle|\enspace a \enspace\middle|\enspace \phi_1 \land \phi_2 \enspace\middle|\enspace \lnot \phi @@ -32,7 +32,7 @@ The $\Sop$-modality is comparable to $\Uop$: $\phi_1\Sop\phi_2$ holds if $\phi_2 \end{definition} \camil -We additionally define $\lor, \rightarrow, \leftrightarrow, \text{false}$ using this syntax as usual. +We additionally define $\lor, \rightarrow, \leftrightarrow, \bot$ using this syntax as usual. The precedence order of the operators borrowed from LTL remains the same. $\Pop$ binds equally strong as $\Xop$ and $\lnot$. @@ -48,7 +48,7 @@ In discourse, it can be helpful to distinguish different kinds of PLTL formulas. \wffp\ (pure past \wff) inductively as the smallest classes conforming to the following rules: \begin{itemize} \item - Atomic propositions and $\text{true}$ are \wffn. + Atomic propositions and $\top$ are \wffn. \item If $\phi,\psi \in \wffn \cup \wfff$, then $\phi \Uop \psi, \Xop\phi \in \wfff$. \item @@ -71,8 +71,8 @@ They can be seen as counterparts of the derived LTL modalities $\square$ and $\l \begin{definition}[Derived PLTL operators] Given $\phi \in PLTL$, then: \begin{equation*} - \Fop^{-1} \phi \defeq \top \Sop \phi \qquad - \Gop^{-1} \phi \defeq \neg \Fop^{-1} \neg \phi + \Fop^{-1} \phi \enspace\defeq\enspace \top \Sop \phi \qquad + \Gop^{-1} \phi \enspace\defeq\enspace \neg \Fop^{-1} \neg \phi \qedhere \end{equation*} \end{definition} |