November 30, 2021
Nicolas Mazzocchi
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.