Muller automaton

From Wikipedia, the free encyclopedia

A Muller automaton is a type of finite automaton accepting infinite strings. The acceptance condition is represented by a set C \subseteq 2^S of subsets of the states. The automaton accepts a run iff the set of states occurring infinitely many times in the run belongs to C.

Contents

[edit] Equivalence with other types of Automata

Büchi automata, parity automata, Rabin Automata, and Streett automata are all subclasses of Muller 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. The equivalence of non-deterministic Büchi automaton and deterministic Muller automaton forms the substance of McNaughton's Theorem. Thus, deterministic and non-deterministic Muller automaton are equivalent in terms of the languages the can accept.

[edit] Büchi automaton

If F is the set of final states in a Büchi automata with the set of states Q and transition function Δ and initial state qinit, we can construct a Muller automata with same set of states, transition function and initial state with the accepting condition as C. C is defined as C = \{X|X \subseteq 2^Q \and X \cap F \neq \emptyset\}

[edit] Rabin automaton

Similarly, the Rabin conditions (Ej,Fj) can be emulated by constructing the acceptance set in the Muller automata as all sets in F \subseteq 2^Q which satisfy F \cap E_j = \emptyset \and F \cap F_j \neq \emptyset, 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.

[edit] Streett automaton

The Streett conditions (Ej,Fj) can be emulated by constructing the acceptance set in the Muller automata as all sets in F \subseteq 2^Q which satisfy F \cap E_j = \emptyset \rightarrow F \cap F_j \neq \emptyset, for some j.