Recherche
En collaboration avec B. Courcelle et M. Kante, je m'intéresse au model-checking de propriétés MS-definissables pour des classes de graphes de clique-width bornée.
Avec M. Kante et D. Soguet, étudiant en thèse au LRI, nous avons testé la possibilité d'utiliser des logiciels tels que MONA, basé sur des automates d'arbres, pour le model-checking de telles propriétés de graphes. Les tests montrent que les automates construits sont souvent de taille trop importante pour que les calculs aboutissent.
Il est donc utile d'examiner d'autres méthodes comme les schémas d'étiquetage. Un schéma d'étiquetage pour une propriété de sommets de graphe, ou une fonction (comme la distance entre deux sommets), attribue aux sommets des étiquettes de " petite " de taille ( O(log(n)) ou O(log 2 (n)) pour un graphe de taille n) qui permettent ensuite de tester la propriété ou de calculer la fonction à partir des étiquettes, sans explorer le graphe. J'ai construit un schéma d'étiquetage général pour des fonctions inductivement calculées dans les graphes de largeur de clique bornée. Ce schéma n'utilise pas les outils logiques de la première méthode. Il permet de tester la propriété ou de calculer la fonction en temps constant à partir des étiquettes.