Vérification et synthèse de modèles algébriques – VeSyAM

Deux célèbres résultats de la théorie des automates et des langages formels sont l'existence d'algorithmes en temps polynomial pour détecter l'égalité de chaînes de caractères compressées et la procédure d'Angluin pour l'apprentissage d'automates déterministes par des questions d'appartenance et d'équivalence. À ce jour, ces deux résultats classiques ont une multitude d'applications, allant de la compression des données à la vérification automatique. Cependant, deux questions fondamentales et étroitement liées restent obstinément ouvertes, à savoir si l'égalité des chaînes compressées peut être résolue par des algorithmes parallèles rapides (i.e. si le problème se situe dans la classe de complexité NC) et si les transducteurs chaîne à chaîne et à états finis peuvent être appris avec une complexité de requête polynomiale.

Dans cette proposition, nous adoptons une nouvelle approche pour ces deux problèmes ouverts, en utilisant l'algèbre et la théorie des nombres. Plus précisément, nous traduisons le problème du test d'égalité de chaînes compressées en une variante du test d'identité de circuit dans l'anneau des entiers cyclotomiques, tandis que nous modélisons les transducteurs de chaînes comme des machines à registre polynomiales. Notre approche s'inspire en partie des récentes percées dans la théorie des automates qui ont été réalisées à l'aide de techniques algébriques. Les solutions à ces problèmes amélioreront considérablement la boîte à outils de ceux qui développent des algorithmes pour manipuler des chaînes compressées (e.g., dans les bases de données génomiques et le traitement XML) ainsi que ceux qui travaillent dans l'analyse de programmes. Notre programme de travail représente une extension ambitieuse des récentes recherches de la porteuse du projet et de ses collaborateurs. La méthodologie fait appel à un large éventail de techniques, allant de la théorie des automates à la théorie des nombres algébriques et à la géométrie algébrique.