Muller Automata

1 files changed, 16 insertions, 0 deletions

diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 8468218..544e0b4 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -166,6 +166,22 @@ The transition relation $\delta : \mathcal{Q} \times 2^{AP} \rightarrow 2^\mathc
 		\end{enumerate}
 \end{itemize}
 
+The next step in the conversion algorithm is converting the B\"uchi Automaton into a deterministic Muller Automaton.
+Let us first define the Muller Automaton:
+\begin{definition}[Deterministic Muller Automaton]
+	A deterministic Muller automaton~\cite{McNaughton1966} is a tuple $A = (\mathcal{Q}, \Sigma, \delta, \mathcal{Q}_0,F)$ where
+	\begin{description}
+		\item[$\mathcal{Q}$] is a finite set of states
+		\item[$\Sigma$] is an alphabet
+		\item[$\delta: \mathcal{Q} \times \Sigma \rightarrow \mathcal{Q}$] is a transition function
+		\item[$\mathcal{Q}_0 \subseteq \mathcal{Q}$] is a set of initial states
+		\item[$\mathcal{F} \subseteq \mathcal{P}(\mathcal{Q})$] is a set of sets of states that define the acceptance condition. $A$ accepts exactly those runs in which the set of infinitely often occurring states in an element of $\mathcal{F}$.
+	\end{description}
+\end{definition}
+
+Converting a NBA to a Muller automaton was shown to be possible by R. McNaughton~\cite{McNaughton1966}
+and is part of what is known as McNaughton's theorem.
+
 \cbend
 %Provide the syntactic algorithm to convert PLTL to LTL
 %TODO: Provide algorithm via automata to convert PLTL to LTL