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 if there exists a run, such that all the states occurring infinitely often in the run are in the final state set. In contrast, a Büchi automaton accepts a word if there exists a run, such that at least one state occurring infinitely often in the final state set.
Co-Büchi automata are strictly weaker than Büchi automata.

Formal definition

Formally, a deterministic co-Büchi automaton is a tuple that consists of the following components:
In a non-deterministic co-Büchi automaton, the transition function is replaced with a transition relation. The initial state is replaced with an initial state set. Generally, the term co-Büchi automaton refers to the non-deterministic co-Büchi automaton.
For more comprehensive formalism see also ω-automaton.

Acceptance Condition

The acceptance condition of a co-Büchi automaton is formally
The Büchi acceptance condition is the complement of the co-Büchi acceptance condition:

Properties

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