Co-Büchi automaton

Formally, a deterministic co-Büchi automaton is a tuple ${\displaystyle {\mathcal {A}}=(Q,\Sigma ,\delta ,q_{0},F)}$ that consists of the following components:

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

In a non-deterministic co-Büchi automaton, the transition function ${\displaystyle \delta }$ is replaced with a transition relation ${\displaystyle \Delta }$. The initial state ${\displaystyle q_{0}}$ is replaced with an initial state set ${\displaystyle Q_{0}}$. Generally, the term co-Büchi automaton refers to the non-deterministic co-Büchi automaton.

For more comprehensive formalism see also ω-automaton.

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.}$

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.}$

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