Inclusion Checking between Büchi Automata

March 31, 2023

Kyveli Doveri


Inclusion Checking between Büchi Automata

Time:   11:00am
Location:   Meeting room 302
Virtual transmission:   Zoom3 https://zoom.us/j/3911012202
Pass:   @s3

In this talk I will present two algorithms to decide the language inclusion problem between Büchi automata. Our approach leverage a notion of quasiorders to prune the search for a counterexample by discarding candidates which are subsumed by others for the quasiorder. Discarded candidates are guaranteed to not compromise the completeness of the algorithm. The first algorithm uses two quasiorders, one for the prefixes and one for the periods of ultimately periodic words. The second algorithm uses a family of right quasiorders that we obtain by adapting the notion of family of right congruences put forward by Maler and Staiger in 1993.