OCD (if this causes conflict, feel free to rollback)

1 files changed, 25 insertions, 18 deletions

diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 6977f4a..1138e11 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -171,7 +171,8 @@ After all, these formulas are meaningless for $\vDash_0$, since (using Gabbay's
 		&\equiv \lnot (\top \Uop (\lnot (c \rightarrow \lnot f \Sop s)))\\
 		&\equiv \lnot (\top \Uop (c \land \lnot (\lnot f \Sop s))).
 	\end{align*}
-	With Gabbay's $\Uop$ and $\Sop$, this becomes (first rewriting the $\Sop$, then the $\Uop$):
+	With Gabbay's $\Uop$ and $\Sop$, this becomes (first rewriting the $\Sop$, then the $\Uop$):%
+		\footnote{We will informally use $\rightarrow$ for rewriting here, reserving $\equiv$ for true equivalence.}
 	\begin{align*}
 		\lnot (\top \Uop (c \land \lnot(\lnot f \Sop s)))
 		&\rightarrow \lnot (\top \Uop (c \land \lnot(s \lor \lnot f \land \lnot f \Sop s)))\\
@@ -382,29 +383,34 @@ 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 Safra's Determinization Algorithm~\citep{Safra1988}.
 
-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.
+Safra's algorithm is an algorithm to determinize B\"uchi automata, based on subset construction.
+This means that we consider sets of states in the original automaton, like we did for the determinization of NFAs described in section 4.1.
+These sets of states we call \emph{macrostates}.
+In this book, we will not describe the underlying theory of Safra's algorithm.
+Instead, we will provide a simple description.
+A more thorough discussion of the algorithm is given by \citet{Roggenbach2002}.
+We will mostly follow this description, with slight modifications.
 
 Let $B = (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 $Q$.
+Safra's algorithm returns an automaton without acceptance criterion where the states are constructed as trees of $Q$.
 Once this automaton is returned,
-an accepting condition must be chosen.
+an acceptance criterion 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 = (Q', \Sigma, q_0', \delta', F')$.
 
-Choose $V := \{1, 2, \dots, 2\cdot|Q|\}$ for denoting nodes in Safra trees.
+Choose $V := \{1, 2, \dots, 2\cdot|Q|\}$ for denoting nodes in Safra trees.%
+	\footnote{Safra trees are defined by \citet{Roggenbach2002}.
+		In short, they are ordered trees with macrostates as labels.}
 
 \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 $q_0'$ is the Safra tree consisting of only the 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$.
+				%TODO: this mark is not mentioned anywhere else right now. Perhaps explain the intuition first.
+			\item For every node $v$ with macrostate $M$ such that $M \cap F \neq \emptyset$, create a new node $v' \in (V\setminus 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.
@@ -413,30 +419,31 @@ Choose $V := \{1, 2, \dots, 2\cdot|Q|\}$ for denoting nodes in Safra trees.
 	\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)
+			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}
 
-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.
+The last step of the algorithm is converting the Muller automaton to an LTL formula based on the decomposition of automata as described by \citet{Maler1994}.
+The decomposition of finite automata was first described by \citet{Krohn1965} and is known as the Krohn-Rhodes theorem.
+This theorem, in combination with the work of \citet{Meyer1969}, allows for the translation of Muller automaton to LTL.
 
 \begin{definition}[Cascade Product~\cite{Maler2010}]
 	Let $A = (Q, \Sigma, \delta)$ be an automaton, and let $B = (Q \times \Sigma, Q', \delta')$ be an automaton such that for all $q \in Q$ and $q' \in Q'$, either $\delta'(q',(q,\sigma))$ is defined for all $\sigma \in \Sigma$ or it is undefined for every $\sigma$.
 	The cascade product $A \circ B$ is the automaton $C = (\Sigma, Q'', \delta'')$ where
 	\[
-		Q'' = \{(q, q') \mid \delta'(q',(q,\sigma))\ is\ defined\}
+		Q'' = \{(q, q') \mid \delta'(q',(q,\sigma)) \ne \bot\}
 	\]
 	and
 	\[
 		\delta''((q,q'),\sigma) = (\delta(q',\sigma),\delta'(q',(q,\sigma)))
+		\qedhere
 	\]
 \end{definition}
 \begin{theorem}[Krohn-Rhodes Theorem]
 	For every automaton $A$ there exists a cascade $C = B_1 \circ B_2 \circ \dots \circ B_n$ such that:
 	\begin{enumerate}
-		\item Each $B_i$ is a permutation-reset automaton\footnote{Definition ommited for brevity}
-		\item There is a homomorphism\footnotemark[10] $\phi$ from $C$ to $A$
+		\item Each $B_i$ is a permutation-reset automaton\footnote{\label{note:definition-omitted}Definition omitted for brevity.}
+		\item There is a homomorphism\footnote{See \cref{note:definition-omitted}.} $\phi$ from $C$ to $A$
 		\item Any permutation in some $B_i$ is homomorphic to a subgroup of the tranformation semigroup of $A$
 	\end{enumerate}
 \end{theorem}