IMDEA Software

IMDEA initiative

Home > Events > Software Seminar Series > 2023 > Inclusion Checking between Büchi Automata

Kyveli Doveri

Friday, March 31, 2023

11:00am Meeting room 302 & Zoom3 (pass: @s3)

Kyveli Doveri, PhD Student, IMDEA Software Institute

Inclusion Checking between Büchi Automata


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.