An ω-regular language that is not accepted by any deterministic Buchi automaton

This example is adapted from Example 4.2 of [Tho90].

References

• W. Thomas, "Automata on infinite objects"

def Cslib.ωLanguage.Example.eventually_zero : ωLanguage (Fin 2)

A sequence xs is in eventually_zero iff xs k = 0 for all large k.

Equations

• Cslib.ωLanguage.Example.eventually_zero = {xs : Cslib.ωSequence (Fin 2) | ∀ᶠ (k : ℕ) in Filter.atTop, xs k = 0}

def Cslib.ωLanguage.Example.eventually_zero_na : Automata.NA.Buchi (Fin 2) (Fin 2)

eventually_zero is accepted by a 2-state nondeterministic Buchi automaton.

Equations

• Cslib.ωLanguage.Example.eventually_zero_na = { Tr := fun (s x s' : Fin 2) => s = 1 → x = 0 ∧ s' = 1, start := {0}, accept := {1} }

theorem Cslib.ωLanguage.Example.eventually_zero_accepted_by_na_buchi : Automata.ωAcceptor.language eventually_zero_na = eventually_zero

theorem Cslib.ωLanguage.Example.eventually_zero_not_omegaLim : ¬∃ (l : Language (Fin 2)), l↗ω = eventually_zero