summaryrefslogtreecommitdiff
path: root/Assignment1/conversion.tex
diff options
context:
space:
mode:
authorErin van der Veen2018-04-15 20:26:27 +0200
committerErin van der Veen2018-04-15 20:26:27 +0200
commit2c379f562d16432383ff34ee308ba1b1b46b7116 (patch)
tree6dedbf65cb747d91ff9dcb5585c880be1b0916d9 /Assignment1/conversion.tex
parentFirst two separation rules (diff)
Elimination Rules
Diffstat (limited to 'Assignment1/conversion.tex')
-rw-r--r--Assignment1/conversion.tex61
1 files changed, 50 insertions, 11 deletions
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 2ed3e47..24be26d 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -27,8 +27,8 @@ This rewrite system is given in Figure~\ref{fig:rewrite}.
&\Xop\phi &&\leftrightarrow \bot \Uop \phi\\
&\Gop\phi &&\leftrightarrow \neg (\top \Uop \neg \phi)\\
&\Fop\phi &&\leftrightarrow \top \Uop \phi\\
- &\Gop^{--1}\phi &&\leftrightarrow \neg (\top \Sop \neg \phi)\\
- &\Fop^{--1}\phi &&\leftrightarrow \top \Sop \neg
+ &\Gop^{-1}\phi &&\leftrightarrow \neg (\top \Sop \neg \phi)\\
+ &\Fop^{-1}\phi &&\leftrightarrow \top \Sop \neg
\end{alignat*}
\caption{The rewrite rules for writing any PLTL formula as a formula containing only $\Sop$ and $\Uop$.}
\label{fig:rewrite}
@@ -42,21 +42,60 @@ Gabby proofs that this can by done in Theorem 2.4 of his paper,
the rewrite rules are given in the Appendix of the same paper.
In this book, we will not proof that these rewrite rules hold, but they are given below.
First, however, note that there are 8 possible cases where there is a $\Uop$ in the scope of a $\Sop$.
-\begin{itemize}
+\begin{enumerate}
\item Suppose $E = q \Sop a \wedge (\alpha \Uop \beta))$ then it holds that $E = E_1 \vee E_2 \vee E_3$ if:
- \begin{align*}
- E_1 &= (q \Sop a) \wedge (\alpha \Sop a) \wedge \alpha (\alpha \Uop \beta)\\
- E_2 &= \beta \wedge (\alpha \Sop a) \wedge (q \Sop a)\\
- E_3 &= q \Sop \beta \wedge q \wedge (\alpha \Sop a) \wedge (q \Sop a)
- \end{align*}
+ \begin{align*}
+ E_1 &= (q \Sop a) \wedge (\alpha \Sop a) \wedge \alpha (\alpha \Uop \beta)\\
+ E_2 &= \beta \wedge (\alpha \Sop a) \wedge (q \Sop a)\\
+ E_3 &= q \Sop \beta \wedge q \wedge (\alpha \Sop a) \wedge (q \Sop a)
+ \end{align*}
- \item Suppose $E = q \Sop a \wedge \neg (a \Uop \beta)$ then it holds that $E = E_1 \vee E_2 \vee E_3$ if:
+ \item Suppose $E = q \Sop a \wedge \neg (\alpha \Uop \beta)$ then it holds that $E = E_1 \vee E_2 \vee E_3$ if:
\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_3 &= a\Sop\neg\beta \wedge \neg \alpha \wedge q \wedge (q \wedge \neg\beta \Sop a)
+ \end{align*}
+
+ \item Suppose $E = q \Sop a \wedge \neg (\alpha \Sop \beta)$ then it holds that $E = E_1 \vee E_2 \vee E_3$ if:
+ \begin{align*}
+ E_1 &= (q \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 &= q \Sop (\neg \beta \wedge \neg \alpha \wedge q \wedge (\neg \beta \wedge q \Sop a))
\end{align*}
-\end{itemize}
+
+ \item Suppose $E = q \vee \neg (\alpha \Uop \beta) \Sop a$ then it holds that $E = \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 it holds that $E = E_1 \vee (E_2 \wedge E_3)$ if:
+ \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)
+ \end{align*}
+
+ \item Suppose $E = q \vee (\alpha \Uop \beta) \Sop a \wedge \neg(\alpha \Uop \beta)$ then it holds that $E = E_1 \vee E_2 \vee E_3$ if:
+ \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)
+ \end{align*}
+
+ \item Suppose $E = q \vee \neg(\alpha \Uop \beta) \Sop a \wedge (\alpha \Uop \beta)$ then it holds that $E = E_1 \vee E_2$ if:
+ \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)
+ \end{align*}
+ Where $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 it holds that $E = \neg \Gop^{-1}(E_1 \vee E_2 \vee E_3)$ if:
+ \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)
+ \end{align*}
+ After elimination of $\Gop^{-1}$, this formula can be further eliminated.
+ In particular by using elimination 5.
+\end{enumerate}
\paragraph{Automata-based Algorithm}