summaryrefslogtreecommitdiff
path: root/Assignment1/conversion.tex
diff options
context:
space:
mode:
authorCamil Staps2018-04-22 22:11:06 +0200
committerCamil Staps2018-04-22 22:11:06 +0200
commit548bb90e218162e331becf8a5ad509738b3c8d6b (patch)
tree7ff3b3b642b97c252c27b6e5e7439f1e614749cd /Assignment1/conversion.tex
parentResolve LaTeX warnings (diff)
Hackfixes to get changebar right
Diffstat (limited to 'Assignment1/conversion.tex')
-rw-r--r--Assignment1/conversion.tex16
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$.