Kyveli Doveri, PhD Student, IMDEA Software Institute
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.