Comprendre les Expressions REgulières, les Automates et la Logique – UNREAL

Ce projet s'inscrit dans le domaine de la théorie des langages réguliers de mots et d'arbres. Son objectif est de comprendre des classes de tels langages. Il propose plusieurs pistes de recherche pour attaquer des problèmes réputés difficiles.

La façon standard de "comprendre" une classe de langages réguliers est le "problème d'appartenance", qui consiste à concevoir un algorithme pour décider si un langage d'entrée est dans la classe ou non. Malgré des avancées continues sur ce problème depuis les années 60, des questions fondamentales restent ouvertes, comme la décidabilité des niveaux des hiérarchies d'alternance de quantificateurs en logique du 1er ordre.

Au cours des dernières années, des avancées ont été réalisées par les participants de ce projet concernant ces hiérarchies. Elles reposent sur une idée clé : considérer des problèmes plus généraux que l'appartenance.

Nos objectifs scientifiques sont :

- sur les mots finis, de comprendre les niveaux des hiérarchies d'alternance de quantificateurs qui nous échappent. Pour cela, nous proposons d'étudier un nouveau problème, défini dans le projet. Nous pensons que sa compréhension permettra d'obtenir des résultats qui semblent hors de portée avec les techniques actuelles.

- de généraliser aux mots infinis ce qui a été obtenu sur les mots finis. Idéalement, nous souhaitons obtenir des réductions des mots infinis aux mots finis. Historiquement, les résultats sur les mots infinis ont toujours été inspirés par ceux obtenus sur les mots finis. Cela rend l'objectif réaliste.

- de développer l'approche pour les langages d'arbres finis. Caractériser des formalismes descriptifs sur les arbres est très difficile (en particulier, le problème d'appartenance pour la logique du 1er ordre semble être hors de portée). Cependant, les résultats obtenus sur les mots concernent des classes considérées comme plus abordables sur les arbres. Cela laisse espérer que la théorie, qui n'existe par actuellement, pourra être développée.