Buchi Automata: Ramsey-based Approach Using Simulation Subsumption
Our tool is called 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. The latest version of the tool additionally uses generalized automata minimization techniques using good approximations of multipebble simulations and trace inclusions (see the POPL 2013 paper listed below).
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. These are implemented in the GOAL tool. However, our experiments indicate that RABIT performs much better and can solve much larger instances than the methods implemented in GOAL.