Muller Automaton - Transformation To Non-deterministic Muller Automaton

Transformation To Non-deterministic Muller Automaton

Following is a list of automata constructions which transforms a type of ω-automata to a non-deterministic muller automaton.

From Büchi automaton

If is the set of final states in a Büchi automata with the set of states, 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 ≠ }

From Rabin automaton/Parity automaton

Similarly, the Rabin conditions can be emulated by constructing the acceptance set in the Muller automata as all sets in which satisfy, 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 can be emulated by constructing the acceptance set in the Muller automata as all sets in which satisfy, for all j.