Definition
A co‑Büchi automaton is a type of ω‑automaton—an abstract machine that processes infinite input words—whose acceptance condition requires that, along a run, only finitely many visits are made to a designated set of “rejecting” states. Formally, a nondeterministic co‑Büchi automaton is a tuple $ \mathcal{A} = (Σ, Q, Q_0, δ, F) $ where
- $ Σ $ is a finite input alphabet,
- $ Q $ is a finite set of states,
- $ Q_0 \subseteq Q $ is the set of initial states,
- $ δ \subseteq Q \times Σ \times Q $ is the transition relation, and
- $ F \subseteq Q $ is the set of rejecting states.
A run $ρ = q_0 q_1 q_2 \dots$ over an infinite word $w = a_0 a_1 a_2 \dots$ is accepting iff the set of states occurring infinitely often in $ρ$ is disjoint from $F$; equivalently, only finitely many positions of the run belong to $F$.
Overview
Co‑Büchi automata are employed primarily in formal verification and automata theory to describe “safety‑type” properties of systems—conditions that must hold eventually forever after a finite number of violations. They constitute one of the simplest acceptance mechanisms for ω‑languages, alongside Büchi, Rabin, Streett, and parity conditions. The complement of a language accepted by a Büchi automaton can be expressed by a co‑Büchi automaton, which motivates the “co‑” prefix.
Nondeterministic co‑Büchi automata are strictly less expressive than nondeterministic Büchi automata; there exist ω‑regular languages (e.g., the set of words containing infinitely many occurrences of a particular symbol) that cannot be recognized by any co‑Büchi automaton. Deterministic co‑Büchi automata are even weaker, recognizing only a proper subset of the languages accepted by their nondeterministic counterparts.
Etymology / Origin
The term is derived from the name of the Swiss mathematician Julius Richard Büchi (1924–1984), who introduced Büchi automata in the 1960s as a model for recognizing sets of infinite sequences (ω‑regular languages). The prefix “co‑” reflects the dual nature of the acceptance condition: while a Büchi automaton requires that some accepting state be visited infinitely often, a co‑Büchi automaton requires that rejecting states be visited only finitely often.
Characteristics
| Aspect | Description |
|---|---|
| Acceptance condition | Finiteness of visits to a designated rejecting set $F$; the run must eventually stay within the complement $Q \setminus F$. |
| Determinism vs. nondeterminism | Both deterministic and nondeterministic variants exist. Nondeterministic co‑Büchi automata are more expressive than deterministic ones, but both are less expressive than Büchi automata. |
| Expressive power | Recognize a strict subclass of ω‑regular languages, namely those that are complements of languages recognizable by nondeterministic Büchi automata. |
| Closure properties | Closed under union, intersection, and complementation (the complement of a co‑Büchi language is Büchi‑recognizable). |
| Decision problems | Emptiness, universality, and language inclusion are decidable; emptiness can be checked in linear time via graph‑reachability analysis. |
| Conversion | A nondeterministic Büchi automaton can be complemented by first converting it to a deterministic parity automaton and then interpreting the parity condition as a co‑Büchi condition, though this may cause an exponential blow‑up. |
| Applications | Model checking of safety properties, synthesis of controllers, verification of liveness‑to‑safety reductions, and as intermediate representations in automata‑theoretic algorithms. |
Related Topics
- Büchi automaton – ω‑automaton with an “infinitely often” acceptance condition.
- Parity automaton – Generalization of Büchi and co‑Büchi using a priority function; subsumes many acceptance conditions.
- Rabin and Streett automata – More expressive ω‑automata with complex acceptance pairs.
- ω‑regular languages – Class of languages of infinite words recognized by various ω‑automata, including co‑Büchi.
- Model checking – Formal verification technique where co‑Büchi automata are used to represent safety specifications.
- Determinization – Process of converting nondeterministic ω‑automata to deterministic ones, often involving a shift from Büchi to parity or co‑Büchi conditions.
This entry follows an encyclopedic style, presenting established facts about co‑Büchi automata without speculation.