summaryrefslogtreecommitdiff
path: root/Assignment1/conversion.tex
diff options
context:
space:
mode:
authorErin van der Veen2018-04-23 21:20:53 +0200
committerErin van der Veen2018-04-23 21:20:53 +0200
commit3ce91bf844723be99e183bee375bf447d9f9b237 (patch)
treef1a5fdb97337e62875f3543cacc5e0255bcdf44e /Assignment1/conversion.tex
parentHackfixes to get changebar right (diff)
Mention that the translation Muller -> LTL lies outside the scope of this book.
Diffstat (limited to 'Assignment1/conversion.tex')
-rw-r--r--Assignment1/conversion.tex5
1 files changed, 3 insertions, 2 deletions
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index fe9b136..be5196f 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -446,14 +446,15 @@ This theorem, in combination with the work of \citet{Meyer1969}, allows for the
\begin{enumerate}
\item Each $B_i$ is a permutation-reset automaton\footnote{\label{note:definition-omitted}Definition omitted for brevity.}
\item There is a homomorphism\footnote{See \cref{note:definition-omitted}.} $\phi$ from $C$ to $A$
- \item Any permutation in some $B_i$ is homomorphic to a subgroup of the tranformation semigroup of $A$
+ \item Any permutation in some $B_i$ is homomorphic to a subgroup of the transformation semigroup of $A$
\end{enumerate}
\end{theorem}
The cascade product can then be used to create star-free regular sets.
These sets can then be transformed into LTL formulae.
+We will not discuss this transformation in detail since it lies beyond the scope of this book.
\cbend
%Provide the syntactic algorithm to convert PLTL to LTL
-%TODO: Provide algorithm via automata to convert PLTL to LTL
+%Provide algorithm via automata to convert PLTL to LTL
%TODO: In both cases make use of examples from SSH Paper