Semi-Deterministic Büchi Automata

1 files changed, 24 insertions, 0 deletions

diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 1786b5d..7635f05 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -245,6 +245,30 @@ Let us first define the Muller Automaton:
 
 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.
+There are multiple ways to convert a NBA to a Muller Automaton.
+In this book we will describe the following method: NBA $\rightarrow$ Semi-deterministic BA $\rightarrow$ Rabin Automaton $\rightarrow$ Muller Automaton.
+\begin{definition}[Semi-deterministic B\"uchi Automaton]
+	A B\"uchi automaton $A$ is semi-deterministic if its set of states $Q$ has two disjoint partitions $D$ and $N$ such that $F \subseteq D$ and for all $d \in D$ automaton $A$ with $F = \{d\}$ is deterministic.
+\end{definition}
+
+Creating a semi-deterministic BA from a NBA is done in the following way:
+
+Let $(\mathcal{Q}, \Sigma, \Delta, \mathcal{Q}_0, F)$ be a B\"uchi automaton.
+The equivalent semi-deterministic B\"uchi automaton is then defined as: $(N \cup D, \Sigma, \Delta', \mathcal{Q}_0', F')$ where:
+\begin{itemize}
+	\item $N = 2^\mathcal{Q}$
+	\item $D = 2^\mathcal{Q} \times 2^\mathcal{Q}$
+	\item $\mathcal{Q}_0' = \{\mathcal{Q}_0\}$
+	\item $\Delta' = \Delta_1 \cup \Delta_2 \cup \Delta_3 \cup \Delta_4$ where:
+		\begin{itemize}
+			\item $\Delta_1 = \{(S, a, S') \mid S' = Pr(S,a)\}$
+			\item $\Delta_2 = \{(S, a, (\{q'\},\emptyset)) \mid \exists_{q \in S} (q,a,q') \in \Delta\}$
+			\item $\Delta_3 = \{((L,R),a,(L',R')) \mid L \neq R \text{ and } L' = Pr(L,a) \text{ and } R'=(L' \cap F) \cup Pr(R,a)\}$
+			\item $\Delta_4 = \{((L,L),a,(L',R')) \mid L' = Pr(L,a) \text{ and } R' = (L' \cap F) \}$
+		\end{itemize}
+	\item $F' = \{(L,L) \mid L \neq \emptyset\}$
+\end{itemize}
+and $Pr: \mathcal{Q} \times \Sigma \rightarrow \mathcal{Q}$ such that $Pr(S,a) = \{q' \mid \exists_{q \in S} (q, a, q') \in \Delta \}$.
 
 \cbend
 %Provide the syntactic algorithm to convert PLTL to LTL