(joint work with Filippo Bonchi)

We present a (hopefully) new algorithm for determining if two non-deterministic finite automata are language equivalent. We exploit coinductive up-to techniques to improve the standard algorithm by Hopcroft and Karp for deterministic finite automata, so as to avoid computing the whole deterministic automata. Although the proposed algorithm remains exponential in worst case (the problem is PSPACE-complete), experimental results show that it can be much faster than the standard algorithm: in most cases, only a very small portion of the underlying deterministic automata has to be explored.