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:

is a finite set. The elements of are called the states of.
is a finite set called the alphabet of.
is the transition function of.
is an element of, called the initial state.
is the final state set. accepts exactly those words with the run, in which all of the infinitely often occurring states in are in.

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.