diff options
Diffstat (limited to 'Assignment1/conversion.tex')
| -rw-r--r-- | Assignment1/conversion.tex | 56 |
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 |