Basic properties of deterministic Buchi automata

Stream: CSLib

[Ching-Tsun Chou]

I created two PRs for proving the basic properties of deterministic Buchi automata. I'd appreciate your reviews. They are:

cslib#150 shows that:

• The ω-language accepted by a deterministic Buchi automaton is the ω-limit of the (finite-word) language accepted by the same automaton.
• The ω-language accepted by a finite-state deterministic Buchi automaton is ω-regular.
• The ω-limit of a regular language is ω-regular.

cslib#152 exhibits an omega-regular language (that is, it is accepted by a finite-state nondeterministic Buchi automaton) that is not accepted by any deterministic Buchi automaton which is not even required to be finite-state. In case you are curious, that language is:

/-- A sequence `xs` is in `eventually_zero` iff `xs k = 0` for all large `k`. -/
def eventually_zero : ωLanguage (Fin 2) :=
  { xs : ωSequence (Fin 2) | ∀ᶠ k in atTop, xs k = 0 }

Proving that it is not the ω-limit of any language was a lot of fun.

[Chris Henson]

I have left a review on cslib#152. (I reviewed everything in the diff so maybe including some of cslib#150, sorry if that is confusing!)

[Ching-Tsun Chou]

Thanks a lot!

[Ching-Tsun Chou]

I closed cslib#150 and included it as part of cslib#152. Chris's comments have been incorporated.

[Ching-Tsun Chou]

BTW, is there a document (paper, presentation, tutorial, etc) on grind?

[Snir Broshi]

Ching-Tsun Chou said:

BTW, is there a document (paper, presentation, tutorial, etc) on grind?

AFAIK this is the go-to document about it, but it's probably still under development

[Ching-Tsun Chou]

Thanks for the info!