Safra's determinization algorithm

1 files changed, 35 insertions, 21 deletions

diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 607d030..5fdc04f 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -339,29 +339,43 @@ 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}
+In this book we will describe Safra's Determinization Algorithm.
 
-Creating a semi-deterministic BA from a NBA is done in the following way:
+%TODO: Safra's algorithm might be used directly?
+Safra's algorithm is an algorithm based on subset construction that is capable of determinizing non-deterministic B\"uchi automata.
+In this book, we will not describe the underlying theory of the algorithm.
+Instead, we will provide you with a simple description.
+A more thorough look into the algorithm can be found in a book by Markus Roggenbach~\cite{Roggenbach2002}.
+We will follow mostly the same description as provided by Roggenbach, with slight modifications.
 
-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 \}$.
+Let $B = (\mathcal{Q}, \Sigma, q_0, \Delta, F)$ be a NBA.
+Safra's algorithm returns an automata without accepting condition where the states are constructed as trees of $\mathcal{Q}$.
+Once this automaton is returned,
+an accepting condition must be chosen.
+Given that we want to construct a Muller Automaton,
+we create a set of sets of states containing trees.
+For the purpose of this book, Safra's algorithm will therefore be considered to return a Muller Automaton $A = (\mathcal{Q}', \Sigma, q_0', \delta, F')$.
+
+Choose $V := \{1, 2, \dots, 2|\mathcal{Q}|\}$ for denoting nodes in Safra trees.
+
+\begin{enumerate}
+	\item $q_0'$ is the Safra tree\footnote{Safra trees are defined in Roggenbachs book.} consisting of node 1 labelled with macrostate $\{q_0\}$.
+	\item For every input $a$ and tree $T$ with set $N$ of nodes,
+		the value of the transition function $\delta(T,a)$ is computed as follows:
+		\begin{enumerate}
+			\item Remove all marks ``!'' in $T$
+			\item For every node $v$ with macrostate $M$ such that $M \cap F \neq \emptyset$, create a new node $v' \in (V\\N)$, such that $v'$ becomes the youngest son of $v$ and carries the macrostate $M \cap F$.
+			\item Perform subset construction on every $v$.
+			\item Perform horizontal merge on every node $v$.
+			\item Remove all nodes with empty macrostates.
+			\item Perform vertical merge on node $v$.
+		\end{enumerate}
+	\item Prune all unreachable states.
+	\item Create $F'$ such that for every subset $S$ of $Q'$ it holds that for some $v \in V$:
+		\[
+			S \in F' \Leftrightarrow (\forall_{\text{Tree } t \in S} v \text{ is in } t) \wedge (\exists_{\text{Tree } t \in S} v \text{ is marked in } t)
+		\]
+\end{enumerate}
 
 \cbend
 %Provide the syntactic algorithm to convert PLTL to LTL