Copy-edited first part of semantic algorithm

1 files changed, 15 insertions, 14 deletions

diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 72304d2..2a3272d 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -260,7 +260,7 @@ The final step of the algorithm entails removing the parts of the formula that c
 
 \erin
 \paragraph{Automata-based Algorithm}
-The Automata-based Algorithm, which we will call the semantic algorithm hence forth, is based on the following translations:
+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
@@ -295,17 +295,17 @@ Particularly, we must extend it with the property in Figure~\ref{fig:log_consist
 Furthermore, we need to modify the generation of the B\"uchi automaton.
 
 Let $\phi$ be an PLTL formua over $AP$.
-Let $\mathcal{G}_\phi = (\mathcal{Q}, 2^{AP}, \delta, \mathcal{Q}_0,\mathcal{F})$ where:
+Let $\mathcal{G}_\phi = (Q, 2^{AP}, \delta, Q_0,\mathcal{F})$ where:
 \begin{itemize}
-	\item $\mathcal{Q}$ is the set of all elementary formulae $B \subseteq closure(\phi)$
-	\item $\mathcal{Q}_0 = \{B \in Q \mid \phi \in B\}$
+	\item $Q$ is the set of all elementary sets of formulae $B \subseteq closure(\phi)$
+	\item $Q_0 = \{B \in Q \mid \phi \in B\}$
 	\item $\mathcal{F} = \{F_{\phi_1 \Uop \phi_2} \mid \phi_1 \Uop \phi_2 \in closure(\phi)\} \cup \{F_{\phi_1 \Sop \phi_2} \mid \phi_1 \Sop \phi_2 \in closure(\phi)\}$ where
 		\begin{align*}
 			F_{\phi_1 \Uop \phi_2} &= \{B \in Q \mid \phi_1 \Uop \phi_2 \not\in B \text{ or } \phi_2 \in B\}\\
 			F_{\phi_1 \Sop \phi_2} &= \{B \in Q \mid \phi_1 \Sop \phi_2 \not\in B \text{ or } \phi_2 \in B\}
 		\end{align*}
 \end{itemize}
-The transition relation $\delta : \mathcal{Q} \times 2^{AP} \rightarrow 2^\mathcal{Q}$ is given by:
+The transition relation $\delta : Q \times 2^{AP} \rightarrow 2^Q$ is given by:
 \begin{itemize}
 	\item If $A \neq B \cap AP$, then $\delta(B,A) = \emptyset$
 	\item If $A = B \cap AP$, then $\delta(B,A)$ is the set of all elementary sets of formulas $B'$ satisfying
@@ -326,17 +326,18 @@ The transition relation $\delta : \mathcal{Q} \times 2^{AP} \rightarrow 2^\mathc
 The next step in the conversion algorithm is converting the B\"uchi Automaton into a deterministic Muller Automaton.
 Let us first define the Muller Automaton:
 \begin{definition}[Deterministic Muller Automaton]
-	A deterministic Muller automaton~\cite{McNaughton1966} is a tuple $A = (\mathcal{Q}, \Sigma, \delta, \mathcal{Q}_0,F)$ where
-	\begin{description}
-		\item[$\mathcal{Q}$] is a finite set of states
-		\item[$\Sigma$] is an alphabet
-		\item[$\delta: \mathcal{Q} \times \Sigma \rightarrow \mathcal{Q}$] is a transition function
-		\item[$\mathcal{Q}_0 \subseteq \mathcal{Q}$] is a set of initial states
-		\item[$\mathcal{F} \subseteq \mathcal{P}(\mathcal{Q})$] is a set of sets of states that define the acceptance condition. $A$ accepts exactly those runs in which the set of infinitely often occurring states in an element of $\mathcal{F}$.
-	\end{description}
+	A deterministic Muller automaton~\cite{McNaughton1966} is a tuple $A = (Q, \Sigma, \delta, Q_0,\mathcal F)$ where
+	\begin{itemize}
+		\item $Q$ is a finite set of states
+		\item $\Sigma$ is an alphabet
+		\item $\delta: Q \times \Sigma \rightarrow Q$ is a transition function
+		\item $Q_0 \subseteq Q$ is a set of initial states
+		\item $\mathcal{F} \subseteq \mathcal{P}(Q)$ is a set of sets of states that define the acceptance condition. $A$ accepts exactly those runs in which the set of infinitely often occurring states in an element of $\mathcal{F}$.
+		\qedhere
+	\end{itemize}
 \end{definition}
 
-Converting a NBA to a Muller automaton was shown to be possible by R. McNaughton~\cite{McNaughton1966}
+Converting NBAs to Muller automata was shown to be possible by \citet{McNaughton1966}
 and is part of what is known as McNaughton's theorem.
 
 \cbend