diff options
author | Erin van der Veen | 2018-04-17 19:32:53 +0200 |
---|---|---|
committer | Erin van der Veen | 2018-04-17 19:32:53 +0200 |
commit | 4a62c5b44d832623cf6655ea4340c500eb7a8d9a (patch) | |
tree | 3b324508d83f66457ed9328da76e497b17080c41 /Assignment1/conversion.tex | |
parent | PLTL to Büchi automaton (diff) |
Muller Automata
Diffstat (limited to 'Assignment1/conversion.tex')
-rw-r--r-- | Assignment1/conversion.tex | 16 |
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 |