Adding Buchi Automaton Model Checking to CSLib?

Stream: CSLib

[Atticus Kuhn]

I am currently working on a project in Lean4 that might be of interest to CSLib, and I would like to ask if the maintainers would be interested in having me add this theory added to CSLib. The work I am doing involves property-based model checking of finite state automata, which is highly relevant to hardware model checking. I have formalised the work of "Verification of concurrent programs: the automata-theoretic framework" by  Moshe Y. Vardi in Lean4. I'm a bit unclear about the scope of CSLib, but I think that people involved in hardware model-checking would be very interested in this formalisation and work. You can see my work so far at:
https://github.com/AtticusKuhn/Transition-System-Ranking-Function/blob/master/Autoomaton/Ordinal2.lean

[Swarat Chaudhuri]

Hi Atticus, we would absolutely love for you to add a formalization of omega-automata (including tree automata). It seems to me that model-checking based on omega-automata might be a bit too specialized and be better done as a separate project that references the omega-automata definitions from CSlib. But this is just my personal opinion.

[Fabrizio Montesi]

Sustained, I'd like to integrate this.

I've received several ideas for automata theory, and all use slightly different definitions. So I'd like to discuss definitions a bit, since there seems to be good potential to share results. I'll open a thread that collects pointers as soon as I have a moment.