Library

NBA · ω-regular

Infinitely often a

@thethinkmachine·version 1·CC BY 4.0·added 28 Sept 2026

The canonical Büchi automaton for GF a: accepts exactly those infinite words containing infinitely many a's. Acceptance is about the cycle the run settles into, not where it stops.

Open in AutomataStudio
More
Open in the desktop app Download the .automaton file Source on GitHub
waitingsaw abaab
The machine as drawn — 2 states, 4 transitions.

The author’s examples, run

(a) → accept(b) → reject(ab) → accepta(b) → rejectb(a) → acceptabab(ab) → accept