summaryrefslogtreecommitdiff
path: root/Assignment1/conversion.tex
diff options
context:
space:
mode:
authorErin van der Veen2018-04-18 13:03:05 +0200
committerErin van der Veen2018-04-18 13:03:05 +0200
commit7b0106beb5284de60f16ea3573f20203915efdc2 (patch)
tree2de1d350e2fae6de3f5e803a2d59854d0a881231 /Assignment1/conversion.tex
parentStart 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.tex24
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