Co-Büchi automaton

In automata theory, a co-Büchi automaton is a variant of Büchi automaton. The only difference is the accepting condition: a Co-Büchi automaton accepts an infinite word w if there exist a run, such that all the states occurring infinitely often in the run are not in the acceptance condition. In contrast, a Büchi automaton accepts a word if there exists a run, such that at least one state occurring infinitely often in its acceptance condition.

Co-Büchi automata are strictly weaker than Büchi automata.

Formal definition

Formally, a deterministic co-Büchi automaton is a tuple A = (Q,Σ,δ,q₀,F) that consists of the following components:

• 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⊆Q is the acceptance condition. A accepts exactly those runs r, in which all of the infinitely often occurring states in r are not in F.

In a non-deterministic co-Büchi 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, co-Büchi automaton refers to non-deterministic co-Büchi Büchi automaton.

For more comprehensive formalism see also ω-automaton.

Properties

Co-Büchi automata are closed under union, intersection, projection and determinization.