diff options
author | Erin van der Veen | 2018-04-18 13:03:05 +0200 |
---|---|---|
committer | Erin van der Veen | 2018-04-18 13:03:05 +0200 |
commit | 7b0106beb5284de60f16ea3573f20203915efdc2 (patch) | |
tree | 2de1d350e2fae6de3f5e803a2d59854d0a881231 /Assignment1/conversion.tex | |
parent | Start with editing of the syntactic algorithm for PLTL -> LTL (diff) |
Semi-Deterministic Büchi Automata
Diffstat (limited to 'Assignment1/conversion.tex')
-rw-r--r-- | Assignment1/conversion.tex | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex index 1786b5d..7635f05 100644 --- a/Assignment1/conversion.tex +++ b/Assignment1/conversion.tex @@ -245,6 +245,30 @@ 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} + +Creating a semi-deterministic BA from a NBA is done in the following way: + +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 \}$. \cbend %Provide the syntactic algorithm to convert PLTL to LTL |