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 : Thursday 23 October 2025 |
|
Contact pour cette page : Cyril.Banderier at lipn.univ-paris13.fr |