HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

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.
Document type :
Complete list of metadata

Cited literature [43 references]  Display  Hide  Download

Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Friday, May 19, 2006 - 7:16:57 PM
Last modification on : Wednesday, April 6, 2022 - 3:48:03 PM
Long-term archiving on: : Tuesday, February 22, 2011 - 11:36:58 AM


  • 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⟩



Record views


Files downloads