IMDEA Software

Iniciativa IMDEA

Inicio > Eventos > Software Seminar Series > 2023 > Inclusion Checking between Büchi Automata
Esta página aún no ha sido traducida. A continuación se muestra la página en inglés.

Kyveli Doveri

viernes 31 de marzo de 2023

11:00am Meeting room 302 & Zoom3 https://zoom.us/j/3911012202 (pass: @s3)

Kyveli Doveri, PhD Student, IMDEA Software Institute

Inclusion Checking between Büchi Automata

Abstract:

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.