From ee10160e3621632071e4274138daba379e5c7f56 Mon Sep 17 00:00:00 2001
From: Erin van der Veen
Date: Thu, 19 Apr 2018 20:15:39 +0200
Subject: Muller to LTL

---
 Assignment1/conversion.tex | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'Assignment1/conversion.tex')

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
-- 
cgit v1.2.3