Résumé : Finite automata are used in a wide range of verification problems. 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".
Dernière modification : Monday 27 May 2024 | Contact pour cette page : Cyril.Banderier at lipn.univ-paris13.fr |