Mu-Calculus Based Resolution of XPath Decision Problems

Pierre Genevès 1 Nabil Layaïda 1
1 WAM - Web, adaptation and multimedia
Inria Grenoble - Rhône-Alpes
Abstract : XPath is the standard declarative notation for navigating XML data and returning a set of matching nodes. In the context of XSLT/XQuery analysis, query optimization, and XML type checking, XPath decision problems arise naturally. They notably include XPath containment (whether or not for any tree the result of a particular query is included in the result of a second one), and XPath satisfiability (whether or not an expression yields a non-empty result), in the presence (or the absence) of XML DTDs. In this paper, we propose a unifying logic for XML, namely the alternation-free modal mu-calculus with converse. We show how to translate major XML concepts such as XPath and DTDs into this logic. Based on these embeddings, we show how XPath decision problems can be solved using a state-of-the-art EXPTIME decision procedure for mu-calculus satisfiability. We provide preliminary experiments which shed light, for the first time, on the cost of solving XPath decision problems in practice.
Type de document :
[Research Report] RR-5868, INRIA. 2006, pp.30
Liste complète des métadonnées
Contributeur : Rapport de Recherche Inria <>
Soumis le : vendredi 19 mai 2006 - 19:16:57
Dernière modification le : samedi 17 septembre 2016 - 01:35:53
Document(s) archivé(s) le : mardi 22 février 2011 - 11:36:58



  • HAL Id : inria-00070158, version 1



Pierre Genevès, Nabil Layaïda. Mu-Calculus Based Resolution of XPath Decision Problems. [Research Report] RR-5868, INRIA. 2006, pp.30. <inria-00070158>



Consultations de
la notice


Téléchargements du document