Merge branch 'master' of gitlab.science.ru.nl:eveen/Model-Checking

2 files changed, 34 insertions, 0 deletions

diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index e474f74..72624e6 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -417,6 +417,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
diff --git a/Assignment1/library.bib b/Assignment1/library.bib
index 2035c70..0da201b 100755
--- a/Assignment1/library.bib
+++ b/Assignment1/library.bib
@@ -1,3 +1,33 @@
+@Article{Meyer1969,
+  title={A note on star-free events},
+  author={Meyer, Albert R},
+  journal={Journal of the ACM (JACM)},
+  volume={16},
+  number={2},
+  pages={220--225},
+  year={1969},
+  publisher={ACM}
+}
+
+@Article{Krohn1965,
+  title={Algebraic theory of machines. I. Prime decomposition theorem for finite semigroups and machines},
+  author={Krohn, Kenneth and Rhodes, John},
+  journal={Transactions of the American Mathematical Society},
+  volume={116},
+  pages={450--464},
+  year={1965},
+  publisher={JSTOR}
+}
+
+@InCollection{Maler2010,
+  title={On the krohn-rhodes cascaded decomposition theorem},
+  author={Maler, Oded},
+  booktitle={Time for verification},
+  pages={260--278},
+  year={2010},
+  publisher={Springer}
+}
+
 @InCollection{Roggenbach2002,
   title={Determinization of B{\"u}chi-automata},
   author={Roggenbach, Markus},