summaryrefslogtreecommitdiff
path: root/Assignment1/conversion.tex
diff options
context:
space:
mode:
authorErin van der Veen2018-04-15 13:55:52 +0200
committerErin van der Veen2018-04-15 13:55:52 +0200
commit9f970a1224bc94e57ad6ce7efd4f2218c9bba4f4 (patch)
treee9a5de6d410077cafa77474e1990dfbff32c0692 /Assignment1/conversion.tex
parentMerge branch 'master' of gitlab.science.ru.nl:eveen/Model-Checking (diff)
Fix rewrite rules
Diffstat (limited to 'Assignment1/conversion.tex')
-rw-r--r--Assignment1/conversion.tex12
1 files changed, 6 insertions, 6 deletions
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index e42d967..9e39283 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -23,12 +23,12 @@ This rewrite system is given in Figure~\ref{fig:rewrite}.
\begin{figure}
\centering
\begin{alignat*}{2}
- &\Pop\phi &&\leftrightarrow \phi \Sop \bot\\
- &\Xop\phi &&\leftrightarrow \phi \Uop \bot\\
- &\Gop\phi &&\leftrightarrow \neg (\neg \phi \Uop \top)\\
- &\Fop\phi &&\leftrightarrow \phi \Uop \top\\
- &\Gop^{--1}\phi &&\leftrightarrow \neg (\neg \phi \Sop \top)\\
- &\Fop^{--1}\phi &&\leftrightarrow \phi \Sop \top
+ &\Pop\phi &&\leftrightarrow \bot \Sop \phi\\
+ &\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
\end{alignat*}
\caption{The rewrite rules for writing any PLTL formula as a formula containing only $\Sop$ and $\Uop$.}
\label{fig:rewrite}