Co-Büchi automaton

Template:Unreferenced 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 $w$ if there exists a run, such that all the states occurring infinitely often in the run are in the final state set $F$. In contrast, a Büchi automaton accepts a word $w$ if there exists a run, such that at least one state occurring infinitely often in the final state set $F$.

(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 $𝒜=(Q,\mathrm{\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 $𝒜$.
• $\mathrm{\Sigma }$ is a finite set called the alphabet of $𝒜$.
• $\delta :Q\times \mathrm{\Sigma }\to Q$ is the transition function of $𝒜$.
• $q_0$ is an element of $Q$, called the initial state.
• $F\subseteq Q$ is the final state set. $𝒜$ 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 $\mathrm{\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

$\mathrm{\exists }i\mathrm{\forall }j:j\ge i\rho (w_j)\in F.$

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

$\mathrm{\forall }i\mathrm{\exists }j:j\ge i\rho (w_j)\in F.$

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, Template:ISBN, p. 133–164.