Logiques, graphes et langages
Logiques et graphes
Responsable : Bruno Courcelle.

Présentation de la direction de recherche

Les méthodes de la Logique et de la Théorie des Langages Formels 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 qui en sont un cas particulier, auquel on peut ajouter les « traces »), 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.

  • Dans la perspective d'étendre aux graphes les méthodes de la Théorie des Langages Formels, la LSOM remplace les automates et permet de définir des transformations qui généralisent les transductions de mots et d'arbres basées sur des automates. Des opérations de composition des graphes permettent de définir très facilement des grammaires algébriques de graphes. Les classes correspondantes sont préservées par transductions. On obtient ainsi une extension robuste (on peut donner à ce terme un sens technique précis) de plusieurs notions fondamentales de la Théorie des Langages.
  • La satisfaisabilité d'une formule de la LSOM par un graphe de largeur arborescente ou de largeur de clique donnée est décidable. Les notions citées plus haut de structuration des graphes sont donc pertinentes par rapport à la LSOM de ce point de vue également.
  • Tous les problèmes que l'on peut spécifier en LSOM et en particulier, beaucoup de problèmes NP-complets peuvent être résolus en temps polynomial (souvent même linéaire) sur des classes de graphes structurés. Cette approche s'étend aux problèmes d'optimisation, de dénombrement et d'énumération. La preuve du théorème général ne fournit pas de possibilité d’implantation à cause de la taille des automates associés aux formules et de la difficulté algorithmique de la décomposition de graphes ayant disons plus de 100 sommets. Une possibilité intéressante en cous d’étude consiste à définir un fragment de la LSOM qui est intéressant du point de vue pratique mais pour lequel les calculs restent concrètement possibles.
  • Beaucoup de concepts de la Théorie des Graphes, tels que les décompositions, les représentations de graphes par des intersections d'objets combinatoires ou géométriques peuvent être formalisés avec fruit en LSOM. Cela s'applique aux graphes dénombrables aussi bien que finis.

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.

  • L’étude des décompositions de graphes est un domaine très riche, aussi bien sur le plan de la Théorie Structurelle des Graphs (mise en avant depuis 30 ans par les travaux de Robertson, Seymour et de leurs continuateurs) que sur celui des applications algorithmiques, liées ou non à la logique. On citera la recherche d’algorithmes efficaces de décomposition, la définition de nouvelles décompositions, notamment pour les hypergraphes et les structures relationnelles, ainsi que de décompositions basées sur les graphes planaires et non plus seulement sur les arborescences. L’équipe travaille aussi sur les résultats de dualité qui permettent de caractériser par obstructions les graphes qui n’ont pas de décomposition de tel ou tel type, et sur les caractérisations de l’existence de décompositions en termes de jeux de poursuite sur les graphes, ce dernier point étant très lié au précédent.
  • La vérification rapide de propriétés de graphes au moyen d’étiquettes attachées aux sommets est un domaine où l’association des décompositions de graphes, de la logique (du premier ordre et du second ordre monadique), et des propriétés de classes particulières de graphes (notamment l’arboricité bornée, la planarité, l’exclusion de mineurs) est particulièrement fructueuse. Cette recherche est faite en étroite collaboration avec l’équipe CombAlgo.

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.

Page mise à jour le 12/10/2012 à 11:44