Muller automaton

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 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 languages. They are named after David E. Muller an American mathematician and computer scientist, who invented them in 1963.

Formally, a deterministic Muller-automaton is a tuple A = (Q,Σ,δ,q₀,F) that consists of the following information:

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₀ is replaced by a set of initial states Q₀. Generally, Muller automaton refers to non-deterministic Muller automaton.

For more comprehensive formalism look at ω-automaton.

The Muller automata are equally expressive as parity automata, Rabin Automata, Streett automata, and non-deterministic 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.

...
Wikipedia