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 [math]\displaystyle{ w }[/math] if there exists a run, such that all the states occurring infinitely often in the run are in the final state set [math]\displaystyle{ F }[/math]. In contrast, a Büchi automaton accepts a word [math]\displaystyle{ w }[/math] if there exists a run, such that at least one state occurring infinitely often in the final state set [math]\displaystyle{ F }[/math].

(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 [math]\displaystyle{ \mathcal{A} = (Q,\Sigma,\delta,q_0,F) }[/math] that consists of the following components:

• [math]\displaystyle{ Q }[/math] is a finite set. The elements of [math]\displaystyle{ Q }[/math] are called the states of [math]\displaystyle{ \mathcal{A} }[/math].
• [math]\displaystyle{ \Sigma }[/math] is a finite set called the alphabet of [math]\displaystyle{ \mathcal{A} }[/math].
• [math]\displaystyle{ \delta : Q \times \Sigma \rightarrow Q }[/math] is the transition function of [math]\displaystyle{ \mathcal{A} }[/math].
• [math]\displaystyle{ q_0 }[/math] is an element of [math]\displaystyle{ Q }[/math], called the initial state.
• [math]\displaystyle{ F\subseteq Q }[/math] is the final state set. [math]\displaystyle{ \mathcal{A} }[/math] accepts exactly those words [math]\displaystyle{ w }[/math] with the run [math]\displaystyle{ \rho(w) }[/math], in which all of the infinitely often occurring states in [math]\displaystyle{ \rho(w) }[/math] are in [math]\displaystyle{ F }[/math].

In a non-deterministic co-Büchi automaton, the transition function [math]\displaystyle{ \delta }[/math] is replaced with a transition relation [math]\displaystyle{ \Delta }[/math]. The initial state [math]\displaystyle{ q_0 }[/math] is replaced with an initial state set [math]\displaystyle{ Q_0 }[/math]. 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

[math]\displaystyle{ \exists i \forall j:\; j\geq i \quad \rho(w_j) \in F. }[/math]

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

[math]\displaystyle{ \forall i \exists j:\; j\geq i \quad \rho(w_j) \in F. }[/math]

Properties

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