Co-Büchi automaton

Formal definition

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

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

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

Acceptance Condition

The acceptance condition of a co-Büchi automaton is formally

\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:

\forall i \exists j:; j\geq i \quad \rho(w_j) \in F.

Properties

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

References

References

1. Boker, Udi. (2010). "The Quest for a Tight Translation of Büchi to co-Büchi Automata". Springer.