From LaBRI - Laboratoire Bordelais de Recherche en Informatique

MF: LogGraph

Equipe Méthodes Formelles
Logiques, graphes et langages
Logiques et graphes
Responsable : Bruno Courcelle.

Présentation

Les méthodes de la logique et de la théorie des langages sont appliquées aux graphes et à d'autres objets combinatoires tels que les cartes qui formalisent les dessins de graphes. Dans ce but, le principal langage logique est la logique du second-ordre monadique (LSOM). Son importance repose sur l'équivalence entre la définissabilité en LSOM d'un ensemble d'arbres, finis ou infinis, et la reconnaissabilité par automate fini. Il n’existe pas de notion satisfaisante d'automate « général » de graphe. Il n’en existe que pour les termes (les mots en sont un cas particulier, auquel on peut ajouter celui des traces de Mazurkiewicz) et les arbres avec racine (ordonnés ou non). Ces notions s’appliquent à des classes d'objets structurés de façon arborescente. Les graphes ne sont pas naturellement structurés. Néanmoins différents types de structuration ont été définis et permettent d'étendre à certaines classes de graphes l'équivalence citée plus haut entre reconnaissabilité et définissabilité logique.

Quatre types de résultats et de thèmes de recherche en découlent.

Tous ces thèmes comportent un grand nombre de problèmes ouverts et d’applications potentielles à des domaines voisins étudiés dans l'équipe. Citons deux sujets particulièrement étudiés.

Ces recherches sont clairement de nature fondamentale, mais elles sont motivées par des applications à la construction d'algorithmes pour vérifier des propriétés de graphes et construire des algorithmes efficaces.

Récupéré sur http://www.labri.u-bordeaux.fr/index.php?n=MF.LogGraph
Page mise à jour le 12/10/2012 à 11:44