Efficient static analysis of XML paths and types

• Published in: Acm Sigplan Notices, vol. 42, p. 342-351
• Publication date: 2007

We 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.

Keywords: modal logic ; satisfiability ; type checking ; XPath ; Mu-Calculus ; Xpath ; Containment

Reference

• EPFL-ARTICLE-179718
• View record in Web of Science

Record created on 2012-07-04, modified on 2016-08-09