Décompositions de graphes, automates programmés et vérification de propriétés exprimées en logique

Les décompositions de graphes liées à la largeur arborescente (tree-width) et à la largeur de clique (clique-width) permettent de construire des algorithmes FPT et XP pour des calculs difficiles (problèmes NP-complets). L'exposé les présentera sous forme d'expressions algébriques.

La notion d' "automate programmé" ("fly-automaton" dans les publis en anglais) permet, dans certains cas, d'implanter les automates, finis mais gigantesques, construits à partir de formules de la logique du second-ordre monadique (LSOM). Elle est utilisable au delà de la LSOM et fournit un cadre formel rigoureux permettant de construire de façon systématique des algorithmes pour des graphes "décomposés", de type FPT ou XP (pour la largeur arborescente et la largeur de clique comme paramètres; il s'agit de "programmation dynamique" ) à partir d'expressions logiques des propriétés et fonctions à décider ou à calculer. (Travail commun avec I. Durand du LaBRI).

B.C et J. Engelfriet, Graph structure and MSOL, Cambridge University press 2012.

B.C. et I. Durand, Automata for the verification of monadic second-order graph properties J. Applied Logic 10 (2012) 368-409. final version

B. C. et I. Durand, Computations by fly-automata beyond MSOL, Preprint, May 2013.