Library

DBA · Deterministic Büchi

Never two a's in a row

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

A deterministic Büchi automaton for G¬(a ∧ Xa). One run per word, and acceptance reduces to never reaching the trap state — the shape most safety properties take.

Open in AutomataStudio
More
Open in the desktop app Download the .automaton file Source on GitHub
okjust saw…deadbabaa, b
The machine as drawn — 3 states, 6 transitions.

The author’s examples, run

(b) → accept(ab) → acceptb(ab) → acceptba(b) → accept(a) → rejectaa(b) → reject(aab) → reject