summaryrefslogtreecommitdiff
path: root/Assignment1/conversion.tex
diff options
context:
space:
mode:
authorErin van der Veen2018-04-19 09:47:31 +0200
committerErin van der Veen2018-04-19 09:47:31 +0200
commit16e6811e4574c3e9fc15b9b2213002918fd25e48 (patch)
treef713f011df12fe587176be64bec655c9b8549e36 /Assignment1/conversion.tex
parentMerge branch 'master' of gitlab.science.ru.nl:eveen/Model-Checking (diff)
Safra's determinization algorithm
Diffstat (limited to 'Assignment1/conversion.tex')
-rw-r--r--Assignment1/conversion.tex56
1 files changed, 35 insertions, 21 deletions
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 607d030..5fdc04f 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -339,29 +339,43 @@ 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.
There are multiple ways to convert a NBA to a Muller Automaton.
-In this book we will describe the following method: NBA $\rightarrow$ Semi-deterministic BA $\rightarrow$ Rabin Automaton $\rightarrow$ Muller Automaton.
-\begin{definition}[Semi-deterministic B\"uchi Automaton]
- A B\"uchi automaton $A$ is semi-deterministic if its set of states $Q$ has two disjoint partitions $D$ and $N$ such that $F \subseteq D$ and for all $d \in D$ automaton $A$ with $F = \{d\}$ is deterministic.
-\end{definition}
+In this book we will describe Safra's Determinization Algorithm.
-Creating a semi-deterministic BA from a NBA is done in the following way:
+%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 $(\mathcal{Q}, \Sigma, \Delta, \mathcal{Q}_0, F)$ be a B\"uchi automaton.
-The equivalent semi-deterministic B\"uchi automaton is then defined as: $(N \cup D, \Sigma, \Delta', \mathcal{Q}_0', F')$ where:
-\begin{itemize}
- \item $N = 2^\mathcal{Q}$
- \item $D = 2^\mathcal{Q} \times 2^\mathcal{Q}$
- \item $\mathcal{Q}_0' = \{\mathcal{Q}_0\}$
- \item $\Delta' = \Delta_1 \cup \Delta_2 \cup \Delta_3 \cup \Delta_4$ where:
- \begin{itemize}
- \item $\Delta_1 = \{(S, a, S') \mid S' = Pr(S,a)\}$
- \item $\Delta_2 = \{(S, a, (\{q'\},\emptyset)) \mid \exists_{q \in S} (q,a,q') \in \Delta\}$
- \item $\Delta_3 = \{((L,R),a,(L',R')) \mid L \neq R \text{ and } L' = Pr(L,a) \text{ and } R'=(L' \cap F) \cup Pr(R,a)\}$
- \item $\Delta_4 = \{((L,L),a,(L',R')) \mid L' = Pr(L,a) \text{ and } R' = (L' \cap F) \}$
- \end{itemize}
- \item $F' = \{(L,L) \mid L \neq \emptyset\}$
-\end{itemize}
-and $Pr: \mathcal{Q} \times \Sigma \rightarrow \mathcal{Q}$ such that $Pr(S,a) = \{q' \mid \exists_{q \in S} (q, a, q') \in \Delta \}$.
+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