en>ChrisGualtieri: /* References */Typo fixing, typos fixed: , → , using AWB

2012-07-25T02:38:24Z

References: Typo fixing, typos fixed: , → , using AWB

New page

In [[automata theory]], a '''Muller automaton''' is a type of an [[ω-automaton]].
The acceptance condition separates a Muller automaton from other ω-automata.
The Muller automata is defined using [[ω-automaton#Acceptance conditions|Muller acceptance condition]], i.e. the set of all states visited infinitely often must be an element of the acceptance set. Both deterministic and non-deterministic Muller automata recognize the [[ω-regular language]]s.

==Formal definition==
Formally, a '''deterministic Muller-automaton''' is a tuple ''A'' = (''Q'',Σ,δ,''q''0,'''F''') that consists of the following information:
* ''Q'' is a [[finite set]]. The elements of ''Q'' are called the ''states'' of ''Q''.
* Σ is a finite set called the ''alphabet'' of ''A''.
* δ: ''Q'' × Σ → ''Q'' is a function, called the ''transition function'' of ''A''.
* ''q''0 is an element of ''Q'', called the initial state.
* '''F''' is a set of sets of states. Formally, '''F''' ⊆ '''P'''(''Q'') where '''P'''(''Q'') is [[powerset]] of ''Q''. '''F''' defines the ''acceptance condition''. ''A'' accepts exactly those runs in which the set of infinitely often occurring states is an element of '''''F'''''

In a '''non-deterministic Muller automaton''', the transition function δ is replaced with a transition relation Δ that returns a set of states and initial state is ''q''0 is replaced by a set of initial states ''Q''0. Generally, Muller automaton refers to non-deterministic Muller automaton.

For more comprehensive formalism look at [[ω-automaton]].

==Equivalence with other ω-automata==

The Muller automata are equally [[Ω-automaton#Expressive power of ω-automata|expressive]] as [[parity automaton|parity automata]], [[Rabin automaton|Rabin Automata]], [[Streett automaton|Streett automata]], and non-deterministic [[Büchi automaton|Büchi automata]], to mention some, and strictly more expressive than the deterministic Büchi automata. The equivalence of the above automata and non-deterministic Muller automata can be shown very easily as the accepting conditions of these automata can be emulated using the acceptance condition of Muller automata. [[McNaughton's Theorem]] demonstrates the equivalence of non-deterministic Büchi automaton and deterministic Muller automaton. Thus, deterministic and non-deterministic Muller automaton are equivalent in terms of the languages they can accept.

==Transformation to non-deterministic muller automaton==

Following is a list of [[automata construction]]s which transforms a type of ω-automata to a non-deterministic muller automaton.

;From [[Büchi automaton]]
:If <math>B</math> is the set of final states in a Büchi automata with the set of states <math>Q</math>, we can construct a Muller automata with same set of states, transition function and initial state with the muller accepting condition as '''F''' = { X | X ∈ 2Q ∧ X ∩ B ≠ <math>\emptyset</math>}

;From Rabin automaton/Parity automaton
:Similarly, the Rabin conditions <math>(E_j,F_j)</math> can be emulated by constructing the acceptance set in the Muller automata as all sets in <math>F \subseteq 2^Q</math> which satisfy <math>F \cap E_j = \emptyset \and F \cap F_j \neq \emptyset</math>, for some j. Note that this covers the case of Parity automaton too, as the Parity acceptance condition can be expressed as Rabin acceptance condition easily.

;From Streett automaton
:The Streett conditions <math>(E_j,F_j)</math> can be emulated by constructing the acceptance set in the Muller automata as all sets in <math>F \subseteq 2^Q</math> which satisfy <math>F \cap E_j = \emptyset \rightarrow F \cap F_j = \emptyset</math>, for all j.

==Transformation to deterministic muller automaton==

;Union of two deterministic muller automaton

;From Büchi automaton
[[McNaughton's Theorem]] provides a procedure to transform non-deterministic Büchi automaton to deterministic Muller automaton.

==References==
*[http://www.tcs.tifr.res.in/~pandya/grad/aut06/lect4.pdf Automata on Infinite Words] Slides for a tutorial by Paritosh K. Pandya.
* Yde Venema (2008) [http://staff.science.uva.nl/~yde/teaching/ml/mu/mu2008.pdf Lectures on the Modal μ-calculus]; the [http://folli.loria.fr/cds/2006/courses/Venema.TheModalMUCalculus.pdf 2006 version] was presented at The 18th European Summer School in Logic, Language and Information

[[Category:Automata theory]]

Chromatographic response function - Revision history

en>ChrisGualtieri: /* References */Typo fixing, typos fixed: , → , using AWB