Liens transverses ENS de Lyon

Actualité de l'ENS de Lyon

Une contribution originale sur le problème classique de l'équivalence des langages

Image absente
Actualité

Résumé

Publi du LIP dans ACM Communications

Description

Filippo Bonchi et Damien Pous, du Laboratoire d'informatique du parallélisme (LIP - ENS de Lyon / Inria / CNRS / Université Lyon 1), viennent de proposer une contribution originale sur le problème classique de l'équivalence des langages reconnus par des automates finis non-déterministes. Leur résultat peut être vu comme une optimisation de l'algorithme de Hopcroft et Karp. Il est publié dans la revue Communications of the ACM (Fév. 2015, Vol. 58, No. 2).
Une vidéo tournée à l'ENS de Lyon par Tom Geller pour l'ACM (Association for Computing Machinery) permet de comprendre les travaux des deux chercheurs.

Hacking Nondeterminism with Induction and Coinduction from CACM on Vimeo.

Les automates finis sont des objets mathématiques permettant de modéliser de nombreux systèmes : pilotes automatiques d'avion, robots, serveurs web, machines à café... Il est souvent important de savoir comparer deux automates : est-ce que la nouvelle machine à café fait au moins ce que l'ancienne savait faire ? Est-ce qu'un pilote automatique satisfait une certaine spécification ? C'est un problème décidable mais difficile : il existe depuis longtemps (1971) des algorithmes pour comparer deux automates, mais ces algorithmes nécessitent d'explorer un nombre de configurations potentiellement exponentiel en la taille des automates de départ.
Non seulement le nouvel algorithme élaboré par Damien Pous et Filipppo Bonchi, tous deux chercheurs dans l'équipe Plume du LIP,  est simple, mais il permet d'éviter cette complexité exponentielle dans la plupart des cas, et donc de traiter de plus gros problèmes.
Cet algorithme s'appuie sur deux techniques mathématiques qui sont duales: induction et coinduction. Intuitivement, la coinduction nous permet d'utiliser un algorithme optimiste, qui explore les automates à l'aveuglette et valide ses décisions a posteriori ; l'induction nous permet de donner des indices à cet algorithme, afin d'éviter l'exploration de branches redondantes.
Sources : Hacking Nondeterminism with Induction and Coinduction, Filippo Bonchi, Damien Pous, Communications of the ACM, Vol. 58 No. 2, Pages 87-95