Muller Automaton - Formal Definition

Formal Definition

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 Q.
• Σ 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 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.