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

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

References

• [W. Thomas, "Automata on infinite objects"][Thomas1990]

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

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

Equations

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

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

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

Equations

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

theorem Cslib.ωLanguage.Example.eventuallyZero_accepted_by_na_buchi : Automata.ωAcceptor.language eventuallyZeroNa = eventuallyZero

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