====== 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).

  - The [[http://perso.ens-lyon.fr/damien.pous/hknt | 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.
  - Automata on finite trees subsume automata on finite words. Thus our [[tasimsub|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.
  - The [[https://github.com/thorstent/Limi/ | 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).
  - The tool [[tools|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 [[http://lit2.ulb.ac.be/alaska/|ALASKA tool]]
or the [[http://goal.im.ntu.edu.tw | GOAL tool]].

=== References ===
  * F. Bonchi and D. Pous. [[http://hal.archives-ouvertes.fr/docs/00/71/66/89/PDF/hkc.pdf | Checking NFA equivalence with bisimulations up to congruence]]. POPL 2013. ACM 2013.
  * A. Bouajjani, P. Habermehl, L. Holik, T. Touili, and T. Vojnar. [[http://www.springerlink.com/content/th5316x6746g8253/|Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata]]. In Proc. of 13th International Conference on Implementation and Application of Automata---CIAA'08, San Francisco, CA, USA, volume 5148 of LNCS, pages 57--67, 2008. Springer-Verlag. An extended version appeared as the [[http://www.fit.vutbr.cz/~vojnar/Publications/bhhtv-nartmc-tr-08.pdf|technical report FIT-TR-2008-001]], FIT BUT, Brno, Czech Republic, 2008.
  * P.A. Abdulla, Y.-F. Chen, L. Holik, R. Mayr, and T. Vojnar. [[http://www.springerlink.com/content/a2g32650q853l185/?p=5a3f698fe2924e98ba116c85fbd7d1d8&pi=13|When Simulation Meets Antichains (On Checking Language Inclusion of NFAs)]]. In Proc. of 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems---TACAS'10, Paphos, Cyprus, volume 6015 of LNCS (the ARCoSS subline), pages 158--174, 2010. Springer-Verlag. An extended version appeared as the [[http://www.fit.vutbr.cz/~holik/pub/FIT-TR-2010-001.pdf|technical report FIT-TR-2010-01]], FIT BUT, Brno, Czech Republic, 2010.
  * L. Holik, O. Lengal, J. Simacek, and T. Vojnar. [[http://www.springerlink.com/content/7058528622w84551/|Efficient Inclusion Checking on Explicit and Semi-Symbolic Tree Automata]]. In Proc. of 9th International Symposium on Automated Technology for Verification and Analysis---ATVA'11, Taipei, Taiwan, volume 6996 of LNCS, pages 243--258, 2011. An extended version appeared as the [[http://www.fit.vutbr.cz/~ilengal/pub/FIT-TR-2011-04.pdf|technical report FIT-TR-2011-04]], FIT BUT, Brno, Czech Republic, 2011. 
  * Richard Mayr, Lorenzo Clemente. [[http://www.inf.ed.ac.uk/publications/report/1414.html | Advanced Automata Minimization.]] POPL 2013. ACM 2013. Extended Technical Report EDI-INF-RR-1414.
  * Pavol Černý, Edmund M. Clarke, Thomas A. Henzinger, Arjun Radhakrishna, Leonid Ryzhyk, Roopsha Samanta, Thorsten Tarrach. [[http://arxiv.org/abs/1505.04533 | From Non-preemptive to Preemptive Scheduling using Synchronization Synthesis.]] CAV 2015. To appear.