Expressivité, satisfiabilité et model checking d’une logique spatiale pour arbres non ordonnés

L’objet de cette thèse est de donner différentes caractérisations formelles d’une logique d’arbres que nous appelons ici logique spatiale. Les motivations initiales de ce travail viennent de la possibilité d’utiliser la logique spatiale en tant que langage d’interrogation de documents semi structurés et typage de documents semi structurés. Ces motivations ont défini les problèmes auxquels nous nous sommes intéressés principalement, à savoir la complexité du model checking et la satisfiabilité de la logique, ainsi que de certaines restrictions de celle-ci. Les motivations secondaires viennent des particularités de cette logique par rapport au cadre d’application envisagé. D’une part, l’interprétation d’une logique spatiale sur des arbres est moins étudiée, en général, que sur d’autres objets tels que les processus mobiles, les tas, les graphes. D’autre part, cette logique s’interprète sur un modèle d’arbres non ordonnés, qui est un modèle pour les données semi structurées et documents XML relativement peu étudié. Toutes ces particularités nous ont amenés à nous intéresser plus à ce qu’on peut appeler le pouvoir d’expression de la logique (pour le modèle d’arbres considéré). Nous rassemblons sous ce terme différentes caractérisations comme la décidabilité de la logique, les types de propriétés qu’elle permet d’exprimer ou non, le coût d’une vérification automatisée de ces propriétés, ainsi qu’une comparaison avec des logiques plus « classiques » sur les arbres.

Nous considérons dans cette thèse des arbres finis étiquetés sur les arêtes par les symboles d’un alphabet dénombrable. Il n’y a pas de borne a priori du nombre de fils qu’un nœud de l’arbre peut avoir, nous parlons alors d’arbre d’arité non bornée. De plus, il n’y a pas d’ordre entre les fils d’un nœud de l’arbre : la seule relation entre nœuds qui est prise en compte étant la relation père-fils ; nous parlons alors d’arbres non ordonnés.

Peu de travaux existent sur des formalismes d’arbres non ordonnés (par rapport aux arbres ordonnés) ; on peut citer la logique CMSO [Courcelle, 1990b] qui capture la notion de reconnaissabilité algébrique pour les arbres non ordonnés ; la logique à traits et les automates à traits [Niehren and Podelski, 1993] qui mettent également en correspondance une notion de définissabilité et de reconnaissabilité sur les arbres non ordonnés ; dans [Colcombet, 2002], une notion d’automates à multiensembles a été introduite pour capturer la notion d’ensembles de termes rationnels modulo l’associativité et la commutativité ; les travaux [Ohsaki, 2001] et [Ohsaki and Takai, 2002] introduisent les automates d’arbres équationnels qui reconnaissent des termes modulo des théories équationnelles et en particulier modulo l’associativité et la commutativité ; les automates à multiarbres [Lugiez, 2003] sont des automates d’arbres qui utilisent des contraintes numériques. A ces formalismes nous pouvons ajouter la logique monadique du second ordre (MSO) sur les graphes qui peut également être interprétée sur des arbres.

L’intérêt grandissant sur la modélisation et l’exploitation des données semi structurées a suscité quelques autres travaux sur les arbres non ordonnés, bien que le modèle prédominant soit celui des arbres ordonnés. Dans ce sens, on peut identifier deux courants. Le premier, qui contient un plus grand nombre de travaux, est celui qui s’est intéressé à la logique des ambients[Cardelli and Gordon, 2000a], ou plutôt à son fragment statique. Le calcul des ambients [Cardelli and Gordon, 2000b] est une algèbre de processus. Les termes de cette algèbre, appelés processus, ont une structure d’arbre qui peut changer dans le temps au fur et à mesure que le processus effectue des calculs. La logique des ambients permet de décrire des propriétés sur ces processus et leur évolution ; le fragment statique de la logique ne s’intéresse qu’à la structure des processus, c’est donc une logique (spatiale) pour arbres. Divers fragments et variantes du fragment statique de la logique des ambients ont été étudiés en vue de la modélisation, l’interrogation et le typage des documents structurés [Cardelli and Ghelli, 2004], [Calcagno et al., 2003], [Dal Zilio and Lugiez, 2003], [Dal Zilio et al., 2004]. Le second groupe de travaux considère une extension de la logique monadique du second ordre avec des contraintes de comptage, représentées par des formules de l’arithmétique de Presburger [Seidl et al., 2003], [Seidl et al., 2004] ; il s’agit de la logique PMSO. On peut également citer, en dehors de ces deux groupes de travaux, l’existence de quelques résultats sur l’utilisation des logiques temporelles pour des arbres non ordonnés [Barcelo and Libkin, 2005]. Une étude de différentes logique pour arbres d’arité non bornée a été effectuée récemment dans [Libkin, 2005].

Une logique est dite spatiale lorsqu’elle possède un opérateur de séparation ou de composition. Cet opérateur permet d’exprimer qu’une structure peut être séparée en deux parties, chacune de ces deux parties pouvant être caractérisée indépendamment de l’autre (par une formule logique). Dans les processus du calcul des ambients par exemple, cette composition est utilisée pour exprimer l’exécution en parallèle de deux processus [Cardelli and Gordon, 2000a]. Sur les graphes, la séparation consiste à partitionner l’ensemble des arêtes du graphe en deux et de considérer les deux graphes définis par chacun des sous ensembles d’arêtes [Cardelli et al., 2002], [Dawar et al., 2004].

La logique que nous étudions ici s’inscrit dans le premier groupe de logiques mentionné ci-dessus, cad les logiques issues de la logique des ambients et appliquées aux documents semistructurés. Plus précisément, nous étudions la logique introduite dans [Cardelli and Ghelli, 2004] et nous l’appelons logique spatiale. Cette logique a été initialement introduite comme la base d’un langage de requêtes pour données semi structurées, le langage TQL [Conforti et al., 2002b]. Elle représente essentiellement le fragment statique de la logique des ambients enrichi avec un opérateur de point fixe et un opérateur de quantification sur les arbres. En plus des connecteurs booléens classiques (disjonction, négation, vérité), cette logique comprend des opérateurs spatiaux, de la quantification et un mécanisme de récursion par l’intermédiaire d’un opérateur de point fixe. Les opérateurs spatiaux permettent de parler de la structure de l’arbre : a[φ] exprime le fait que l’arbre a une seule arête partant de la racines et qui mène vers un sous arbre satisfaisant φ ; φ1 | φ2 exprime que l’arbre peut être obtenu en fusionnant les racine de deux arbres, l’un satisfaisant φ1 et l’autre satisfaisant φ2. Ce dernier opérateur est appelé composition et représente une des particularité des logiques spatiales. La quantification dans la logique permet de quantifier sur des étiquettes et sur des arbres. Quant à l’opérateur de point fixe, il ajoute un mécanisme de récursion permettant, par exemple, d’exprimer des régularités dans les chemins de l’arbre, des répétitions d’un motif exact ou approché dans l’arbre, d’exprimer que « quelque part dans l’arbre » φ est vérifié, ou bien « partout où φ1 est vérifié, φ2 l’est aussi » et beaucoup d’autres.

Grâce à la multitude d’opérateurs, cette logique spatiale est très expressive. On peut considérer qu’elle englobe tous les fragments et variantes de la logique des ambients qui ont été cités plus haut, et qui ont été étudiés pour une application aux données semi-structurés. Par ailleurs, certains résultats connus pour la logique des ambients s’appliquent directement à la logique spatiale. Par exemple, nous savons que la satisfiabilité de cette logique n’est pas décidable en présence de quantification [Charatonik and Talbot, 2001, Charatonik et al., 2003]. De plus, le langage TQL dispose d’une implémentation [Conforti et al., 2002a], ce qui laisse croire que le problème de model checking de la logique est décidable, au moins pour le fragment utilisé dans le langage de requêtes TQL.

Table des matières

Introduction
1 Définitions de base
1.1 Multiensembles
1.2 Arithmétique de Presburger
1.3 Modèle d’arbres et représentations des arbres
2 Automates
2.1 Automates de Presburger
2.2 Automates à contraintes numériques
2.2.1 Exécution d’un automate et calcul d’une exécution
2.2.2 Automate déterministe et automate complet
2.2.3 Sous classes d’automates à contraintes numériques
2.3 Propriétés des automates à contraintes numériques
2.3.1 Déterminisation
2.3.2 Clôture par les opérations booléennes
2.3.3 Clôture par homomorphisme
2.3.4 Test du vide
2.3.5 Test d’appartenance
2.4 Propriétés des automates à contraintes numériques sans étoile et semilinéaires
2.4.1 Déterminisation
2.4.2 Clôture par les opérations booléennes
2.4.3 Clôture par homomorphisme
2.4.4 Test du vide
2.4.5 Test d’appartenance
3 Logiques
3.1 Logique monadique du second ordre et extension
3.1.1 Logique monadique du second ordre (MSO)
3.1.2 Logique MSO de Presburger (PMSO)
3.1.3 Logiques monadiques du second ordre et automates à contraintes numériques
3.2 Logique spatiale (LS)
3.2.1 Syntaxe
3.2.2 Sémantique
3.2.3 Opérateurs dérivés
3.2.4 Propriétés de la satisfiabilité
3.2.5 Fragments et variantes de la logique
3.2.6 Exemples
Conclusion

Télécharger le rapport complet