Checking NFA equivalence with bisimulations up to congruence

Abstract : 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. We compare our algorithm to the recently introduced antichain algorithms, by analysing and relating the two underlying coinductive proof methods. We give concrete examples where we exponentially improve over antichains; experimental results moreover show non negligible improvements on random automata.
Type de document :
Communication dans un congrès
Principle of Programming Languages (POPL), Jan 2013, Roma, Italy. ACM, pp.457-468, 2013, 〈10.1145/2429069.2429124〉
Liste complète des métadonnées

Littérature citée [32 références]  Voir  Masquer  Télécharger

https://hal.archives-ouvertes.fr/hal-00639716
Contributeur : Damien Pous <>
Soumis le : mercredi 11 juillet 2012 - 09:47:56
Dernière modification le : mercredi 29 juillet 2015 - 01:14:08

Fichier

hkc.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Filippo Bonchi, Damien Pous. Checking NFA equivalence with bisimulations up to congruence. Principle of Programming Languages (POPL), Jan 2013, Roma, Italy. ACM, pp.457-468, 2013, 〈10.1145/2429069.2429124〉. 〈hal-00639716v5〉

Partager

Métriques

Consultations de
la notice

583

Téléchargements du document

2081