Master
Décidabilité des requêtes XPath avec contraintes de comptage
L’émergence du langage XML comme un standard pour l’échange de données structurées, a rendu nécessaire l’optimisation du langage XPath utilisé pour rechercher et extraire des informations des documents XML. C’est dans ce contexte qu’intervient mon travail de master, qui consiste à définir une logique auquelle se réduisent les problèmes de décidabilité (inclusion, équivalence, jointure et satisfaisabilité) des requêtes XPath avec contraintes de comptage. Pouvoir décider ce type de problèmes en un temps raisonnable permet d’aider à manipuler avec sûreté et efficacité les données XML et peut contribuer à réduire considérablement l’évaluation des requêtes XPath.
La contribution principale de mon travail est la définition d’une nouvelle logique capable de supporter l’expressivité des requêtes XPath avec contraintes de comptage. Cette logique est dérivée de la logique PDL (Propositional Dynamic Logic) et du mu-calcul modal, ce qui permet de tirer profit des résultats déjà établis pour ces logiques. La logique proposée est assez expressive pour supporter, outre la navigation ultidirectionnelle dans les arbres XML, les contraintes de comptage XPath ainsi que d’autres types d’expressions avancées qui ne figurent pas dans la spécification XPath 2.0 telles que les chemins conditionnées, les chemins itératifs et la clôture réflexive sur les chemins.
La principale application de mon travail est un compilateur qui interprète les requêtes XPath en formules de la logique proposée afin de décider de leur satisfaisabilité via le solveur présenté dans les travaux de Genevès [Genevès, 2006].