Sujet : Mots infinis, automates et logique

Responsable : Bruno Courcelle

Téléphone : 05 40 00 60 86, Bureau 117

e-mail : courcell@labri.fr

Équipe :Modélisation et vérification - Logiques, graphes et langages

Thème : Description de mots infinis indexés sur des ensembles totalement ordonnés autres que l’ensemble des entiers naturels par les automates finis, des expressions régulières et les formules logiques.

 

Présentation du sujet :

Les langages, ensembles de mots finis,  peuvent être décrits par des automates finis, des expressions rationnelles et des formules de la Logique du Second-Ordre Monadique. Ces descriptions sont équivalentes en ce sens que l’on peut passer de l’une à l’autre par des algorithmes.

Les mots finis ont été généralisés en mots infinis : suites de lettres indexées par l’ensemble N des entiers naturels, l’ensemble Z des entiers, l’ensemble Q des nombres rationnels, ou plus généralement tout ensemble totalement ordonné dénombrable.

Ces mots infinis peuvent également être décrits par  des automates ou des expressions rationnelles : c’est ce que montrent deux articles de V. Bruyère et O. Carton et de A. Bès et O. Carton.

Le travail consiste à lire ces deux articles, d’en synthétiser les principaux résultats et d’examiner la question suivante :

Dans quelle mesure est-ce que la Logique du Second-Ordre Monadique est équivalente à ces formalismes ?

 

Mot-clés : Logique, Automate, expression rationnelle, ensemble ordonné dénombrable.

Références :

V. Bruyère et O. Carton : Automata on linear orderings, 2004

http://www.labri.fr/perso/courcell/CoursMaster/BruyereCarton.ps

A Bès et O. Carton : A Kleene Theorem for Languages of words indexed by linear orderings.

http://www.labri.fr/perso/courcell/CoursMaster/BesCarton.ps

Commentaires éventuels :

Ces questions pourront faire l’objet d’une continuation en thèse. En effet, la décomposition modulaire des graphes dénombrables (étudiée par B. Courcelle et C. Delhommé) utilise des arbres infinis non standard analogues aux mots infinis considérés dans ces articles. La comparaison envisagée dans ce stage entre logique et  automates pourra être étendue aux arbres infinis qui décrivent les décompositions modulaires des graphes dénombrables