On Equivalence Checking of Nondeterministic Finite Automata


     Chen Fu, Yuxin Deng, David N. Jansen, and Lijun Zhang

We provide a comparative study of some typical algorithms
for language equivalence in nondeterministic finite automata and various
combinations of optimization techniques.We find that their practical
effficiency mostly depends on the density and the alphabet size of the
automaton under consideration. Based on our experiments, we suggest to
use HKC (Hopcroft and Karp's algorithm up to congruence) if the
density is large and the alphabet is small; otherwise, we recommend the
antichain algorithm (Wulf, Doyen, Henzinger, Raskin). Bisimulation
equivalence and memoisation both pay off in general. When comparing
highly structured automata over a large alphabet, one should use
symbolic algorithms.