diff options
| -rw-r--r-- | Assignment1/conversion.tex | 16 | ||||
| -rwxr-xr-x | Assignment1/library.bib | 11 |
2 files changed, 27 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 diff --git a/Assignment1/library.bib b/Assignment1/library.bib index 6555f23..7b74626 100755 --- a/Assignment1/library.bib +++ b/Assignment1/library.bib @@ -1,3 +1,14 @@ +@Article{McNaughton1966, + title={Testing and generating infinite sequences by a finite automaton}, + author={McNaughton, Robert}, + journal={Information and control}, + volume={9}, + number={5}, + pages={521--530}, + year={1966}, + publisher={Elsevier} +} + @InProceedings{Maler1990, title={Tight bounds on the complexity of cascaded decomposition of automata}, author={Maler, Oded and Pnueli, Amir}, |