From a0cbbca6b29a423abbc55ee7da62026c115cd8d1 Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Wed, 18 Apr 2018 20:40:20 +0200
Subject: Check syntactic elimination rules
---
Assignment1/conversion.tex | 55 +++++++++++++++++++++++++++-------------------
1 file changed, 33 insertions(+), 22 deletions(-)
(limited to 'Assignment1/conversion.tex')
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 3f4cf0f..4feb094 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -92,12 +92,12 @@ For the proofs of the equivalences, we refer the reader to the appendix of \cite
\erin
\begin{enumerate}[resume]
\item Suppose $E = q \Sop (a \wedge \neg (\alpha \Uop \beta))$, then $E \equiv E_1 \vee E_2 \vee E_3$ where:
- % TODO Verify all except 3
\begin{align*}
- E_1 &= (a \wedge \neg \beta \Sop a) \wedge \neg \beta \wedge \neg (\alpha \Uop \beta)\\
- E_2 &= \neg \beta \wedge \neg \alpha \wedge (\neg \beta \wedge q \Sop a)\\
- E_3 &= a\Sop\neg\beta \wedge \neg \alpha \wedge q \wedge (q \wedge \neg\beta \Sop a)
+ E_1 &= \bot \Sop a\\
+ E_2 &= (\beta \lor \alpha \land \alpha \Uop \beta) \land (\neg a \lor \neg c) \Sop a\\
+ E_3 &= \neg(\beta \lor \alpha \land \alpha \Uop \beta) \land (\neg a \lor \neg c) \Sop a \land (\neg a \land \neg\beta) \Sop (\neg q \land \neg a)
\end{align*}
+ where $c = (\neg a \land \neg\beta) \Sop (\neg q \land \neg a) \land \neg\alpha \land \neg\beta$.
\item Suppose $E = q \Sop (a \wedge \neg (\alpha \Uop \beta))$, then $E \equiv E_1 \vee E_2 \vee E_3$ where:
\begin{align*}
@@ -106,43 +106,54 @@ For the proofs of the equivalences, we refer the reader to the appendix of \cite
E_3 &= q \Sop (\neg \alpha \wedge \neg \beta \wedge q \wedge (\neg \beta \wedge q) \Sop a)
\end{align*}
- \item Suppose $E = (q \vee \neg (\alpha \Uop \beta)) \Sop a$, then $E \equiv \neg (\neg a \Sop \neg q \wedge (\alpha \Uop \beta) \wedge \neg a) \wedge \Fop^{-1} a$,
+ \item Suppose $E = (q \vee \neg (\alpha \Uop \beta)) \Sop a$,
+ then $E \equiv \neg (\neg a \Sop (\neg q \wedge (\alpha \Uop \beta) \wedge \neg a)) \wedge \Fop^{-1} a$,
which can be reduced via rule 1.
- \item Suppose $E = (q \vee \alpha \Uop \beta) \Sop (a \wedge \alpha \Uop \beta)$, then $E \equiv E_1 \vee (E_2 \wedge E_3)$ where:
+ \item Suppose $E = (q \vee \alpha \Uop \beta) \Sop (a \wedge \alpha \Uop \beta)$, then $E \equiv E_1 \lor E_2 \lor E_3$ where:
\begin{align*}
- E_1 &= (\alpha \Sop a) \wedge (\beta \vee (\alpha \wedge (\alpha \Uop \beta)))\\
- E_2 &= (\beta \vee \alpha \vee \neg(\neg\beta \Sop \neg q) \Sop \beta \wedge (\alpha \Sop a))\\
- E_3 &= (\beta \vee (\alpha \wedge (\alpha \Uop \beta))) \vee \neg (\neg\beta \Sop \neg q)
+ E_1 &= \alpha \Sop a \wedge (\beta \vee \alpha \wedge \alpha \Uop \beta)\\
+ E_2 &= \beta \lor \alpha \land \alpha\Uop\beta \land \neg (\neg\alpha \land \neg\beta \land \neg\beta\Sop\neg q) \Sop (\beta \land \alpha \Sop a)\\
+ E_3 &= \neg (\neg\alpha \land \neg\beta \land \neg\beta\Sop\neg q) \Sop (\beta \land \alpha \Sop a) \land (\beta \vee \alpha \wedge \alpha \Uop \beta) \land \neg (\neg\beta \Sop \neg q)
\end{align*}
\item Suppose $E = (q \vee \alpha \Uop \beta) \Sop (a \wedge \neg(\alpha \Uop \beta))$, then $E \equiv E_1 \vee E_2 \vee E_3$ where:
\begin{align*}
- E_1 &= (\neg \beta \wedge q \Sop a) \wedge \neg \beta \wedge \neg \alpha\\
- E_2 &= q \vee (\alpha \Uop \beta) \Sop \neg \beta \wedge \neg \alpha \wedge (q \vee (\alpha \Uop \beta)) \wedge (\neg \beta \wedge q \Sop a)\\
- E_3 &= (q \wedge \neg \beta \Sop a) \wedge \neg \beta \wedge \neg (\alpha \Uop \beta)
+ E_1 &= ((\neg \beta \wedge q) \Sop a) \wedge \neg \alpha \wedge \neg \beta\\
+ E_2 &= [q \vee \alpha \Uop \beta] \Sop [\neg \alpha \wedge \neg \beta \wedge (q \vee \alpha \Uop \beta) \wedge (\neg \beta \wedge q) \Sop a]\\
+ E_3 &= (q \wedge \neg \beta) \Sop a \wedge \neg \beta \wedge \neg (\alpha \Uop \beta)
\end{align*}
+ $E_2$ has a $\Uop$ in a $\Sop$, but can be further rewritten using elimination 5.
\item Suppose $E = (q \vee \neg(\alpha \Uop \beta)) \Sop (a \wedge \alpha \Uop \beta)$, then $E \equiv E_1 \vee E_2$ where:
\begin{align*}
- E_1 &= (q \vee \neg (\alpha \Uop \beta) \Sop \beta \wedge (q \vee \neg (\alpha \Uop \beta)) \wedge (\alpha \wedge q \Sop a))\\
- E_2 &= (\alpha \wedge q \Sop a) \wedge \alpha \wedge (\alpha \Uop \beta)
+ E_1 &= [q \vee \neg (\alpha \Uop \beta)] \Sop [\beta \wedge (q \vee \neg (\alpha \Uop \beta)) \wedge (\alpha \wedge q) \Sop a]\\
+ E_2 &= (\alpha \wedge q) \Sop a \wedge \alpha \wedge \alpha \Uop \beta
\end{align*}
$E_1$ can be further reduced using eliminations 8 and 4.
- \item Suppose $E = (q \vee \neg (\alpha \Uop \beta)) \Sop (a \wedge \neg (\alpha \Uop \beta))$, then $E \equiv \neg \Gop^{-1}(E_1 \vee E_2 \vee E_3)$ where:
+
+ \item Suppose $E = (q \vee \neg (\alpha \Uop \beta)) \Sop (a \wedge \neg (\alpha \Uop \beta))$, then $E \equiv \neg (E_1 \vee E_2 \vee E_3)$ where:
\begin{align*}
- E_1 &= \neg a \vee \neg (\alpha \Uop \beta)\\
- 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)
+ E_1 &= \square^{-1} (\neg a \vee \alpha \Uop \beta)\\
+ 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*}
- After elimination of $\Gop^{-1}$, this formula can be further eliminated, in particular using elimination 5.
+ \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
+ 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}
+ The term\erin\ $E_3$ (and $E_2$) can be further eliminated, in particular using elimination 5.
+ \cbend{}
\end{enumerate}
+\erin
Note that these rules can only be applied when a $\Uop$ is within the scope of a $\Sop$.
-In order to move the $\Sop$ out of the scope of the $\Uop$, consider that $\Sop$ and $\Uop$ are symmetrical.
-These equivalences also hold when the path is reversed, so similar elimination rules exist for the case that $\Sop$ occurs within the scope of $\Uop$.
+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$.
-The final step of the algorithm entails removing the parts of the formula that contains the $\Sop$-operators.
+The final step of the algorithm entails removing the pure past formulas from the boolean combination.
+After all, these formulas are meaningless for $\vDash_0$, since (using Gabbay's definitions) these formulas can only say things about exclusive past time.
\camil
\begin{example}[A property for an Authentication System]
--
cgit v1.2.3