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$.

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.

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 $Delta$ and initial state $q\_\{init\}$, 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\; in\; 2^Q\; and\; X\; cap\; F\; neq\; emptyset\}$

Rabin automaton

Similarly, the Rabin conditions $(E\_j,F\_j)$ 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.

Streett automaton

The Streett conditions $(E\_j,F\_j)$ 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.