diff options
| author | Erin van der Veen | 2018-04-19 20:15:49 +0200 |
|---|---|---|
| committer | Erin van der Veen | 2018-04-19 20:15:49 +0200 |
| commit | 531b892a0ceea85e1bbd635950dd7daf9059e95f (patch) | |
| tree | 18f0c7e8845d33f7dd9f72adca2a1563e2b977a4 /Assignment1/conversion.tex | |
| parent | Muller to LTL (diff) | |
| parent | Minor textual enhancements; remove outdated todos (diff) | |
Merge branch 'master' of gitlab.science.ru.nl:eveen/Model-Checking
Diffstat (limited to 'Assignment1/conversion.tex')
| -rw-r--r-- | Assignment1/conversion.tex | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex index 5eb9dba..72624e6 100644 --- a/Assignment1/conversion.tex +++ b/Assignment1/conversion.tex @@ -20,7 +20,11 @@ The syntactic algorithm as proposed by Gabbay has its foundation in the followin For this paragraph we will use Gabbay's definitions.} \begin{enumerate} \item Every PLTL formula can be written using no other temporal operators than $\Sop$ and $\Uop$ operators. - \item Every formula $\phi$ containing only the $\Sop$ and $\Uop$ operators can be written as a boolean combination of $\wfff \cup \wffp \cup \wffn$. + \item Every formula $\phi$ containing only the $\Sop$ and $\Uop$ operators can be written as a boolean combination of $\wfff \cup \wffp \cup \wffn$.% + \footnote{% + This is known as the Separation Theorem. + It was originally proven by \citet{Gabbay1980}. + Folklore has it that when Hans Kamp, a philosopher working on temporal logics, heard of the result, he went out and bought Gabbay a cake (\url{https://cstheory.stackexchange.com/a/29452}, retrieved April 19, 2018).} \item The same formula without past modalities $\psi$, a boolean combination of $\wfff \cup \wffn$, is initially equivalent to $\phi$. \end{enumerate} When these facts are considered in sequence, |