diff options
author | Camil Staps | 2018-04-22 22:11:06 +0200 |
---|---|---|
committer | Camil Staps | 2018-04-22 22:11:06 +0200 |
commit | 548bb90e218162e331becf8a5ad509738b3c8d6b (patch) | |
tree | 7ff3b3b642b97c252c27b6e5e7439f1e614749cd /Assignment1/conversion.tex | |
parent | Resolve LaTeX warnings (diff) |
Hackfixes to get changebar right
Diffstat (limited to 'Assignment1/conversion.tex')
-rw-r--r-- | Assignment1/conversion.tex | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex index 1138e11..fe9b136 100644 --- a/Assignment1/conversion.tex +++ b/Assignment1/conversion.tex @@ -10,7 +10,7 @@ This algorithm is described in more detail below. \label{pltl:to-ltl:syntactic} The syntactic algorithm as proposed by Gabbay has its foundation in the following three facts:% \footnote{% - Note that Gabbay used a slightly different, \enquote{non-strict} definition for the $\Uop$ and $\Sop$ operators. + Gabbay used a slightly different, \enquote{non-strict} definition for the $\Uop$ and $\Sop$ operators. \camil We then get $\sigma \vDash_i \phi_1 \Uop \phi_2 \Leftrightarrow \exists_{j > i}[\sigma \vDash_j \phi_2]$ and $\sigma \vDash_k \phi_1$ for all $i < k < j$ (rather than $i \le k < j$), and similarly for $\Sop$. Thus, our $\phi \Uop \psi$ is equivalent to Gabbay's $\psi \lor \phi \land \phi \Uop \psi$. @@ -92,9 +92,10 @@ For the proofs of the equivalences, we refer the reader to the appendix of \cite \end{align*} The reasoning behind the other elimination rules is similar and will not be discussed in detail. \end{remark} +\cbend -\erin \begin{enumerate}[resume] + \erin \item Suppose $E = (q \lor \alpha\Uop\beta) \Sop a$, then $E \equiv E_1 \vee E_2 \vee E_3$ where: \begin{align*} E_1 &= \bot \Sop a\\ @@ -142,16 +143,17 @@ For the proofs of the equivalences, we refer the reader to the appendix of \cite E_2 &= (\neg a \vee \alpha \Uop \beta) \Sop (\neg q \wedge \alpha \Uop \beta \wedge \neg a)\\ E_3 &= (\neg a \vee \alpha \Uop \beta) \Sop (\neg q \wedge \alpha \Uop \beta) \end{align*} + \camil - Since $\sigma \vDash_i E_2$ entails $\sigma \vDash_i E_3$ for all $i\in\mathbb N$, we also have $E \equiv \neg(E_1 \lor E_3)$.\cbend% - \footnote{\cbcolor{red}\cbstart + Since $\sigma \vDash_i E_2$ entails $\sigma \vDash_i E_3$ for all $i\in\mathbb N$, we also have $E \equiv \neg(E_1 \lor E_3)$.% + \footnote{% According to \citet[p.~439]{Gabbay1989}, $E_3$ is \enquote{subsumed by} $E_2$. - Assuming the straightforward understanding of subsumption ($\phi$ subsumes $\psi$ if and only if $\textsl{Words}(\phi) \supseteq \textsl{Words}(\psi)$), this is incorrect and $E_2$ is subsumed by $E_3$ instead.\cbend} + Assuming the straightforward understanding of subsumption ($\phi$ subsumes $\psi$ if and only if $\textsl{Words}(\phi) \supseteq \textsl{Words}(\psi)$), this is incorrect and $E_2$ is subsumed by $E_3$ instead.} The term\erin\ $E_3$ (and $E_2$) can be further eliminated, in particular using elimination 5. - \cbend{} + \cbend \end{enumerate} -\erin +\erin Note that these rules can only be applied when a $\Uop$ is within the scope of a $\Sop$. In order to move an $\Sop$ out of the scope of a $\Uop$, consider that $\Sop$ and $\Uop$ are symmetrical. The above equivalences also hold when the path is reversed, so similar elimination rules exist for the case that $\Sop$ occurs within the scope of $\Uop$. |