diff options
author | Erin van der Veen | 2018-04-15 13:55:52 +0200 |
---|---|---|
committer | Erin van der Veen | 2018-04-15 13:55:52 +0200 |
commit | 9f970a1224bc94e57ad6ce7efd4f2218c9bba4f4 (patch) | |
tree | e9a5de6d410077cafa77474e1990dfbff32c0692 /Assignment1/conversion.tex | |
parent | Merge 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.tex | 12 |
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} |