Library

NPA · ω-regular

Infinitely often a, or eventually always c

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

A nondeterministic parity automaton that forks between two conditions on its first symbol. Nondeterminism is a convenience here — NPA = DPA — unlike under Büchi.

Open in AutomataStudio
More
Open in the desktop app Download the .automaton file Source on GitHub
guessA: last …A: last …C: last …C: last …ab, ca, bcab, cab, cca, bca, b
The machine as drawn — 5 states, 18 transitions.

The author’s examples, run

(a) → accept(c) → accept(ab) → acceptab(c) → accept(ac) → accept(b) → reject(bc) → rejectabc(b) → reject