Parity automaton

Summary

Redirect to:

A parity automaton is a tuple P = (Σ,Q,q_0, δ, κ) where κ is a mapping κ-: Q → {1, . . . , k} of the states to a number in a given bounded set {1, . . . , k}, which we refer to as colors (and we refer to κ(q), for a state q, as the color of q). For a subset Q_0 ⊆ Q, we use κ(Q_0 ) for the set {κ(q) | q ∈ Q0}.

A run r of a parity automaton is accepting if the minimal color in κ(Inf(r)) is odd.