Lalala

1 files changed, 10 insertions, 11 deletions

diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 8919366..5b97530 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -299,13 +299,13 @@ After all, these formulas are meaningless for $\vDash_0$, since (using Gabbay's
 The Automata-based Algorithm, which we will call the semantic algorithm henceforth, is based on the following translations:
 \begin{enumerate}
 	\item PLTL formulas can be converted to B\"uchi automata~\cite{Lichtenstein1985}
-	\item B\"uchi automata can be converted to deterministic Muller automata
+	\item B\"uchi automata can be converted to deterministic Muller automata~\citep{Safra1988}
 	\item Muller automata can be converted to LTL formulae~\cites{Maler1990, Maler1994}
 \end{enumerate}
 
-Converting an LTL formula to a B\"uchi automata is discussed in Section 5.2 of this book.
+Converting an LTL formula to a B\"uchi automaton is discussed in Section 5.2 of this book.
 Much of this algorithm is the same,
-we must just modify some figures and definitions in order to be able to apply it on PLTL formulae.
+we only need to modify some figures and definitions in order to be able to apply it on PLTL formulae.
 The first Definition we must change is 5.35:
 \begin{definition}[Elementary Sets of PLTL Formulas]
 	$B \subseteq closure(\phi)$ is \emph{elementary} if it is consistent with respect to propositional logic, maximal, and locally consistent with respect to the until and since operators.
@@ -376,29 +376,28 @@ Let us first define the Muller Automaton:
 Converting NBAs to Muller automata was shown to be possible by \citet{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 Safra's Determinization Algorithm.
+In this book we will describe Safra's Determinization Algorithm~\citep{Safra1988}.
 
-%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}$.
+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$.
 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')$.
+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|\mathcal{Q}|\}$ for denoting nodes in Safra trees.
+Choose $V := \{1, 2, \dots, 2\cdot|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:
+		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$.
@@ -410,7 +409,7 @@ Choose $V := \{1, 2, \dots, 2|\mathcal{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}