3 files changed, 50 insertions, 2 deletions
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 75ac71f..1221952 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -374,8 +374,47 @@ 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.
-\cbend
+<<<<<<< HEAD
+There are multiple ways to convert a NBA to a Muller Automaton.
+In this book we will describe Safra's Determinization Algorithm.
+
+%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 $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
 %TODO: Provide algorithm via automata to convert PLTL to LTL
 %TODO: In both cases make use of examples from SSH Paper
diff --git a/Assignment1/library.bib b/Assignment1/library.bib
index e3a11f8..5f9fbcb 100755
--- a/Assignment1/library.bib
+++ b/Assignment1/library.bib
@@ -1,3 +1,12 @@
+@InCollection{Roggenbach2002,
+  title={Determinization of B{\"u}chi-automata},
+  author={Roggenbach, Markus},
+  booktitle={Automata logics, and infinite games},
+  pages={43--60},
+  year={2002},
+  publisher={Springer}
+}
+
 @Article{McNaughton1966,
   title={Testing and generating infinite sequences by a finite automaton},
   author={McNaughton, Robert},
diff --git a/Assignment1/syntax.tex b/Assignment1/syntax.tex
index 7ffa813..81a7d7f 100644
--- a/Assignment1/syntax.tex
+++ b/Assignment1/syntax.tex
@@ -2,7 +2,7 @@
 \erin
 % Provide formal syntax
 % Provide intuitive semantics
-%TODO: Provide formal semantics
+% Provide formal semantics
 This subsection describes the syntax of PLTL.
 PLTL uses the same operators as LTL and adds two additional operators:
 	$\Pop$ (pronounced \enquote{previously}) and