Authors: Filippo
Bonchi and Damien Pous.
We introduce "bisimulation up to congruence" as a technique for proving language equivalence of nondeterministic finite automata. Exploiting this technique, we devise an optimisation of the classical algorithm by Hopcroft and Karp. We compare our algorithm to the recently introduced antichain algorithms, by analysing and relating the two underlying coinductive proof methods. We give concrete examples where we exponentially improve over antichains; experimental results moreover show non negligible improvements on random automata.
We used the Coq proof assistant to formalise most results presented in the paper (up to equivalence/congruence/similarity techniques, the rewriting system to compute the congruence closure, the coinductive proof techniques underlying the two antichain algorithms, the facts that HKC/HKC' can mimick AC/AC', and that AC can mimick HKC on disjoint inclusionsonly the proofs for the concrete examples are missing.)
Here is an HTML version of the development; here is the raw proof script (to be processed with Coq v8. 4).
An implementation of Hopcroft and Karp's algorithm for NFA (HK) and of our optimised version (HKC) can be found here. This is the code we used for the experiments presented in the paper. The modelchecking automata we used can be obtained from Lukas Holik's page: we tested the inclusions of the last 16 consecutive pairs of each sequence, in both directions.
Other implementations of language inclusion or equivalence algorithms for finite automata can be found at LanguageInclusion.org. See for instance libvata for tree automata, and RABIT for infinite word automata.
The various algorithms can be tested online, using the following applet. It suffices to write your favourite NFA in the text field below. (See below for syntax and clickable examples.)

Strong similarity: 
In the HK and HKC columns, the word on the lefthand side is the word corresponding to the current pair; blue pairs are those that are added to the bisimulation upto candidate; grey pairs are those that are skipped according to the other ones. When checking inclusions, arrows of the form X < Y denote pairs of the form X+Y  Y.
The AC column corresponds to the antichainbased algorithm proposed in this paper for CAV'06. Similarly, blue pairs are those added to the antichain and grey ones are those that are skipped (note that some of the blue pairs are removed in the actual antichain when they are subsumed by a subsequent pair).
HKC  AC  HK 

Click on the examples below to load them in the above applet.