FORQ-based Language Inclusion Formal Testing

TL;DR

This paper introduces FORQ-based algorithms for deciding language inclusion between nondeterministic Büchi automata, leveraging novel quasiorders to improve scalability and efficiency over existing methods.

Contribution

It presents a new family of right quasiorders (FORQs) for pruning search space in language inclusion checks, with a specific instantiation called the structural FORQ.

Findings

FORKLIFT outperforms state-of-the-art tools on various benchmarks.

The FORQ-based approach maintains correctness while improving scalability.

Application to program verification and theorem proving benchmarks demonstrates practical effectiveness.

Abstract

We propose a novel algorithm to decide the language inclusion between (nondeterministic) B\"uchi 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 the structural FORQ, induced by the B\"uchi automaton to the right of the inclusion sign. The resulting implementation, called FORKLIFT, scales up better than the state-of-the-art on a variety of benchmarks including benchmarks from program verification and theorem proving for word combinatorics.