a Buchi automaton
/ BUE-khee /
Every finite automaton you have met so far reads a finite string and then stops and decides. But what about a system that never stops — an operating system, a network protocol, a controller that runs forever? Its behaviour is an infinite sequence of events, an infinite word. A Buchi automaton is a finite automaton retooled to accept (or reject) infinite words, making it the natural tool for reasoning about non-terminating, ongoing systems.
It looks exactly like an ordinary nondeterministic finite automaton — states, transitions, a start state, a set of accepting states — but its acceptance condition is reinterpreted for an input that never ends. A run of a Buchi automaton on an infinite word is an infinite path through the states. The acceptance rule is: the run is accepting if it visits some accepting state infinitely often. Not just once, but again and again forever. So instead of asking 'did we finish in an accepting state?', we ask 'did we keep returning to a good state without end?'. This perfectly captures liveness properties like 'the system responds to every request eventually' and fairness like 'this process gets scheduled infinitely often'.
Buchi automata sit at the heart of automatic verification (model checking). They are the bridge between automata and temporal logic: a temporal-logic specification of how a system should behave over infinite time can be translated into a Buchi automaton, and checking the system against the spec becomes a question about these automata. One honest subtlety worth flagging: unlike finite-word automata, nondeterministic Buchi automata are strictly more expressive than deterministic ones — you cannot always determinize a Buchi automaton (you must move to a richer acceptance condition, like Rabin or parity, to determinize). The neat DFA-equals-NFA equivalence does not carry over to infinite words.
A two-state Buchi automaton over the alphabet {req, ack} can express 'every request is eventually acknowledged' as a recurring-good-state condition: stay in a 'waiting' state while a request is unanswered, return to a 'satisfied' accepting state on each ack. An infinite run is accepted only if it keeps revisiting the satisfied state infinitely often — meaning acks never stop coming, so no request is ignored forever.
A Buchi automaton accepts an infinite word if its run visits an accepting state infinitely often.
Buchi acceptance is 'visits an accepting state infinitely often', NOT 'ends in one' — infinite words have no end. And unlike finite-word automata, nondeterministic Buchi automata are strictly more powerful than deterministic ones; you cannot always determinize them.