Checking NFA equivalence with bisimulations up to congruence (Damien Pous)

Damien Pous (LIP, CNRS & ENS Lyon) joint work with Filippo Bonchi

We introduce "bisimulation up to congruence" as a technique for proving language equivalence of non-deterministic finite automata. Exploiting this technique, we devise an optimisation of the classical algorithm by Hopcroft and Karp which, as we show, is exploiting a weaker "bisimulation up to equivalence" technique. The resulting algorithm can be exponentially faster than the recently introduced "antichain algorithms".