diff options
Diffstat (limited to 'Assignment1/conversion.tex')
| -rw-r--r-- | Assignment1/conversion.tex | 25 |
1 files changed, 24 insertions, 1 deletions
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex index 9e39283..2ed3e47 100644 --- a/Assignment1/conversion.tex +++ b/Assignment1/conversion.tex @@ -33,7 +33,30 @@ This rewrite system is given in Figure~\ref{fig:rewrite}. \caption{The rewrite rules for writing any PLTL formula as a formula containing only $\Sop$ and $\Uop$.} \label{fig:rewrite} \end{figure} -This full expressiveness of $\Uop$ and $\Sop$ is proven in theorem 2.3 of the paper by Gabbay~\cite{Gabbay1989}. +This full expressiveness of $\Uop$ and $\Sop$ is proven in the PhD. thesis of J. Kamp~\cite{Kamp1968}, +and again by Gabbay using a different method~\cite{Gabbay1989}. + +Step 2 of the algorithm entails rewriting the formula containing only $\Uop$ and $\Sop$ to a form where there is no $\Sop$ in the scope of a $\Uop$, +and there exists on $\Uop$ in the scope of a $\Sop$. +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} + \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*} + + \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: + \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) + \end{align*} +\end{itemize} \paragraph{Automata-based Algorithm} |