IMDEA Software

IMDEA initiative

Home > Events > Software Seminar Series > 2021 > FORQ-based Language Inclusion Formal Testing

Nicolas Mazzocchi

Tuesday, November 30, 2021

11:00am Lecture hall 1 & Zoom3 https://zoom.us/j/3911012202 (pass: 5551337)

Nicolas Mazzocchi, Post-doctoral Researcher, IMDEA Software Institute

FORQ-based Language Inclusion Formal Testing

Abstract:

We provide a simple and efficient in practice algorithm to decide the language inclusion between (nondeterministic) Büchi automata, a PSpace-complete problem. Our approach, like others before, leverage a notion of quasiorder 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 novelty of our work lies in the quasiorder used to discard candidates. We introduce FORQs (family of right quasiorders) that we obtain by adapting the notion of family of right congruences put forward by Maler and Staiger in 1993. We define a FORQ-based inclusion algorithm which we prove correct and instantiate it for a specific FORQ called structural FORQ induced by the Büchi automata to the right of the inclusion sign. The resulting implementation, called Forklift, almost always outperforms the state-of-the-art on a variety of benchmarks including benchmarks from program verification and theorem proving for word combinatorics.