Geneves, PierreLayaida, NabilSchmitt, Alan2012-07-042012-07-042012-07-04200710.1145/1250734.1250773https://infoscience.epfl.ch/handle/20.500.14299/83482WOS:000253409000034We present an algorithm to solve XPath decision problems under regular tree type constraints and show its use to statically type-check 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 mu-calculus without greatest fixpoint, restricted to finite trees, and where formulas are cycle-free.modal logicsatisfiabilitytype checkingXPathMu-CalculusXpathContainmenttext::journal::journal article::research article