summaryrefslogtreecommitdiff
path: root/Assignment1/conversion.tex
diff options
context:
space:
mode:
authorErin van der Veen2018-04-19 20:15:39 +0200
committerErin van der Veen2018-04-19 20:15:39 +0200
commitee10160e3621632071e4274138daba379e5c7f56 (patch)
treee1d03db9a39e5c26f2d83f4e316807d01df9baa7 /Assignment1/conversion.tex
parentLalala (diff)
Muller to LTL
Diffstat (limited to 'Assignment1/conversion.tex')
-rw-r--r--Assignment1/conversion.tex4
1 files changed, 4 insertions, 0 deletions
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 5b97530..5eb9dba 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -413,6 +413,10 @@ Choose $V := \{1, 2, \dots, 2\cdot|Q|\}$ for denoting nodes in Safra trees.
\]
\end{enumerate}
+The last step of the algorithm is converting the Muller automaton to an LTL formula based on the decomposition of automata as described by O. Maler and A. Pnueli~\cite{Maler1994}.
+The decomposition of finite automata was first described by K. Krohn and J. Rhodes as is known as the Krohn-Rhodes theorem~\cite{Krohn1965}.
+This theorem, in combination with the work of A. Meyer~\cite{Meyer1969} allows for the translation of Muller automaton to LTL.
+
\cbend
%Provide the syntactic algorithm to convert PLTL to LTL
%TODO: Provide algorithm via automata to convert PLTL to LTL