Buchi Automata

Here are some current tools for checking language inclusion of nondeterministic Buchi automata.

• GOAL tool. There are many other methods for checking Buchi automata inclusion/equivalence, e.g., Safra-based constructions, Muller-Schupp constructions, Safra-Pieteman construction, and Slice-based constructions. The GOAL tool implements many of these. On most instances RABIT performs better than GOAL, and thus it can solve much larger instances.
• FORKLIFT. It uses a subsumption-based technique, different from the Ramsey-based method. See CAV'22 paper and the full version of the paper and some benchmarks. The older BAIT tool by same authors uses similar methods, see CONCUR 2021 paper.
• RABIT (Ramsey-based Buchi automata Inclusion Testing). It implements a generalized version of the Ramsey-based method for Buchi automata inclusion checking with additional subsumption techniques using backward and forward simulation preorder. Newer versions of the tool additionally use generalized automata minimization techniques using good approximations of multipebble simulations and trace inclusions (see the LMCS 2019 on the RABIT tool page).

Note: Subsumption-based techniques and simulation-based techniques are very different from each other. Thus the performance of the above tools can vary a lot between different (classes of) instances. I.e., instances that are hard for one tool may be easy for another, and vice-versa. So you might want to try out different tools, to see what works best for your particular automata.