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 . (Deterministic) Co-Büchi automata are strictly weaker than (nondeterministic) 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. Finite automata