Muller automaton

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

• Q is a finite set. The elements of Q are called the states of A.
• Σ is a finite set called the alphabet of A.
• δ: Q × Σ → Q is a function, called the transition function of A.
• q₀ 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 the initial state q₀ is replaced by a set of initial states Q₀. Generally, 'Muller automaton' refers to a non-deterministic Muller automaton.

For more comprehensive formalisation 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 and vice versa.

McNaughton's theorem demonstrates the equivalence of non-deterministic Büchi automaton and deterministic Muller automaton. Thus, deterministic and non-deterministic Muller automata are equivalent in terms of the languages they can accept.

Following is a list of automata constructions that each transforms a type of ω-automata to a non-deterministic Muller automaton.

From Büchi automata

If ${\displaystyle B}$ is the set of final states in a Büchi automaton with the set of states ${\displaystyle Q}$, we can construct a Muller automaton with same set of states, transition function and initial state with the Muller accepting condition as F = { X | X ∈ P(Q) ∧ X ∩ B ≠ ${\displaystyle \emptyset }$}.

From Rabin automata/parity automata

Similarly, the Rabin conditions ${\displaystyle (E_{j},F_{j})}$ can be emulated by constructing the acceptance set in the Muller automaton as all sets ${\displaystyle F\subseteq Q}$ that satisfy ${\displaystyle F\cap E_{j}=\emptyset }$ and ${\displaystyle F\cap F_{j}\neq \emptyset }$, for some j. Note that this covers the case of parity automata too, as the parity acceptance condition can be expressed as a Rabin acceptance condition easily.

From Streett automata

The Streett conditions ${\displaystyle (E_{j},F_{j})}$ can be emulated by constructing the acceptance set in the Muller automaton as all sets ${\displaystyle F\subseteq Q}$ that satisfy ${\displaystyle F\cap F_{j}=\emptyset \implies F\cap E_{j}=\emptyset }$, for all j.

From Büchi automaton

McNaughton's theorem provides a procedure to transform any non-deterministic Büchi automaton into a deterministic Muller automaton.

• Automata on Infinite Words Slides for a tutorial by Paritosh K. Pandya.
• Yde Venema (2008) Lectures on the Modal μ-calculus; the 2006 version was presented at The 18th European Summer School in Logic, Language and Information