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
![{\displaystyle \exists i\forall j:\;j\geq i\quad \rho (w_{j})\in F.}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
The Büchi acceptance condition is the complement of the co-Büchi acceptance condition:
![{\displaystyle \forall i\exists j:\;j\geq i\quad \rho (w_{j})\in F.}](data:image/gif;base64,R0lGODlhAQABAIAAAAAAAP///yH5BAEAAAAALAAAAAABAAEAAAIBRAA7)
Properties
Co-Büchi automata are closed under union, intersection, projection and determinization.
Literature
- Wolfgang Thomas: Automata on Infinite Objects. In: Jan van Leeuwen (Hrsg.): Handbook of Theoretical Computer Science. Band B: Formal Models and Semantics. Elsevier Science Publishers u. a., Amsterdam u. a. 1990, ISBN 0-444-88074-7, p. 133–164.