Finite Automata

The following tools are state-of-the-art for checking language inclusion/equivalence for finite automata on finite words (i.e., regular languages).

  1. The HKC tool by Damien Pous and Filippo Bonchi uses a technique based on bisimulation modulo congruence (see POPL 2013 paper below), and can solve inclusion/equivalence for finite-word automata. Very good performance on most examples.
  2. Automata on finite trees subsume automata on finite words. Thus our tools for tree-automata (libvata) can solve this problem. It mainly uses antichain methods, though it can additionally use simulation subsumption techniques. Libvata is a highly optimized tree-automata library that can perform many other operations besides inclusion checking.
  3. The Limi tool by Pavol Černý, Edmund M. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, Thorsten Tarrach, uses basic antichain methods (without simulation subsumption) to solve NFA language inclusion. Moreover, it can also solve (restricted cases of) NFA inclusion modulo certain permutations of symbols by a specified independence relation. (See forthcoming paper in CAV 2015 below).
  4. The tool RABIT is mainly for checking inclusion of Buchi-automata. However, it can also solve inclusion of finite-word automata. Just invoke the RABIT tool with the option -finite, in addition to the other recommended options. It mainly uses automata minimization techniques based on generalized lookahead-simulation relations. RABIT comes in a bundle with the Reduce-tool that can minimize Buchi automata and finite-word automata (again use the option -finite for finite-word automata).

You might also try the older ALASKA tool or the GOAL tool.


nfasimsub.txt · Last modified: 2015/05/29 02:17 by rmayr