Limiting Until in Ordered Tree Query Languages

作者：Benedikt Michael^*; Ley Clemens^*

来源：ACM Transactions on Computational Logic, 2016, 17(2): 14.

DOI：10.1145/2856104

• Trees
• temporal logic
• hierarchy
• xml

Marx and de Rijke have shown that the navigational core of the w3c XML query language XPath is not first-order complete; that is, it cannot express every query definable in first-order logic over the navigational predicates. How can one extend XPath to get a first-order complete language? Marx has shown that Conditional XPath-an extension of XPath with an "Until" operator-is first-order complete. The completeness argument makes essential use of the presence of upward axes in Conditional XPath. We examine whether it is possible to get "forward-only" languages that are first-order complete for Boolean queries on ordered trees. It is easy to see that a variant of the temporal logic CTL* is first-order complete; the variant has path quantifiers for downward, leftward, and rightward paths, while along a path one can check arbitrary formulas of Linear Temporal Logic (LTL). This language has two major disadvantages: It requires path quantification in both horizontal directions (in particular, it requires looking backward at the prior siblings of a node), and it requires the consideration of formulas of LTL of arbitrary complexity on vertical paths. This last is in contrast with Marx's Conditional XPath, which requires only the checking of a single Until operator on a path. We investigate whether either of these restrictions can be eliminated. Our main results are negative ones. We show that if we restrict our CTL* language by having an Until operator in only one horizontal direction, then we lose completeness. We also show that no restriction to a "small" subset of LTL along vertical paths is sufficient for first-order completeness. Smallness here means of bounded "Until Depth," a measure of complexity of LTL formulas defined by Etessami and Wilke. In particular, it follows from our work that Conditional XPath with only forward axes is not expressively complete; this extends results proved by Rabinovich and Maoz in the context of infinite unordered trees.

• 出版日期2016-3