summaryrefslogtreecommitdiff
path: root/Assignment1/conversion.tex
diff options
context:
space:
mode:
authorCamil Staps2018-04-22 21:06:02 +0200
committerCamil Staps2018-04-22 21:06:02 +0200
commit66bf033eca9975aed38a456ad383ce005fea62d3 (patch)
tree98bfda0b90ec673512e6214365dcea5d6cdf5b97 /Assignment1/conversion.tex
parentAdd very tiny explenation of cascade product and Krohn-Rhodes Theorem (diff)
OCD (if this causes conflict, feel free to rollback)
Diffstat (limited to 'Assignment1/conversion.tex')
-rw-r--r--Assignment1/conversion.tex43
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}