XPath Typing Using a Modal Logic with Converse for Finite Trees

9 years 11 months ago
XPath Typing Using a Modal Logic with Converse for Finite Trees
We present an algorithm to solve XPath decision problems under regular tree type constraints and show its use to statically typecheck XPath queries. To this end, we prove the decidability of a logic with converse for finite ordered trees whose time complexity is a simple exponential of the size of a formula. The logic corresponds to the alternation free modal µ-calculus without greatest fixpoint restricted to finite trees where formulas are cycle-free. Our proof method is based on two auxiliary results. First, XML regular tree types and XPath expressions have a linear translation to cycle-free formulas. Second, the least and greatest fixpoints are equivalent for finite trees, hence the logic is closed under negation. With these proofs, we describe a practically effective system for solving the satisfiability of a formula. The system has been experimented with some decision problems such as XPath emptiness, containment, overlap, and coverage, with or without type constraints. Th...
Pierre Genevès, Nabil Layaïda, Alan Sc
Added 30 Oct 2010
Updated 30 Oct 2010
Type Conference
Year 2007
Authors Pierre Genevès, Nabil Layaïda, Alan Schmitt
Comments (0)