summaryrefslogtreecommitdiff
path: root/Assignment1/conversion.tex
diff options
context:
space:
mode:
authorErin van der Veen2018-04-17 19:32:53 +0200
committerErin van der Veen2018-04-17 19:32:53 +0200
commit4a62c5b44d832623cf6655ea4340c500eb7a8d9a (patch)
tree3b324508d83f66457ed9328da76e497b17080c41 /Assignment1/conversion.tex
parentPLTL to Büchi automaton (diff)
Muller Automata
Diffstat (limited to 'Assignment1/conversion.tex')
-rw-r--r--Assignment1/conversion.tex16
1 files changed, 16 insertions, 0 deletions
diff --git a/Assignment1/conversion.tex b/Assignment1/conversion.tex
index 8468218..544e0b4 100644
--- a/Assignment1/conversion.tex
+++ b/Assignment1/conversion.tex
@@ -166,6 +166,22 @@ The transition relation $\delta : \mathcal{Q} \times 2^{AP} \rightarrow 2^\mathc
\end{enumerate}
\end{itemize}
+The next step in the conversion algorithm is converting the B\"uchi Automaton into a deterministic Muller Automaton.
+Let us first define the Muller Automaton:
+\begin{definition}[Deterministic Muller Automaton]
+ A deterministic Muller automaton~\cite{McNaughton1966} is a tuple $A = (\mathcal{Q}, \Sigma, \delta, \mathcal{Q}_0,F)$ where
+ \begin{description}
+ \item[$\mathcal{Q}$] is a finite set of states
+ \item[$\Sigma$] is an alphabet
+ \item[$\delta: \mathcal{Q} \times \Sigma \rightarrow \mathcal{Q}$] is a transition function
+ \item[$\mathcal{Q}_0 \subseteq \mathcal{Q}$] is a set of initial states
+ \item[$\mathcal{F} \subseteq \mathcal{P}(\mathcal{Q})$] is a set of sets of states that define the acceptance condition. $A$ accepts exactly those runs in which the set of infinitely often occurring states in an element of $\mathcal{F}$.
+ \end{description}
+\end{definition}
+
+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.
+
\cbend
%Provide the syntactic algorithm to convert PLTL to LTL
%TODO: Provide algorithm via automata to convert PLTL to LTL