How big must complete XML query languages be?

ABSTRACT

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 firstorder 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 XML Boolean queries. 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.

REFERENCES

• 1: Pablo Barcelo, Temporal Logics over Unranked Trees, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, p.31-40, June 26-29, 2005 [doi>10.1109/LICS.2005.51]
• 2: Michael Benedikt and Alan Jeffrey. Efficient and Expressive Tree Filters. In FSTTCS, 2007.
• 3: Mikolaj Bojanńzyk, Effective characterizations of tree logics, Proceedings of the twenty-seventh ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, June 09-12, 2008, Vancouver, Canada [doi>10.1145/1376916.1376925]
• 4: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 5: Kousha Etessami , Thomas Wilke, An Until hierarchy and other applications of an Ehrenfeucht-Fraïssé game for temporal logic, Information and Computation, v.160 n.1-2, p.88-108, July 10/Aug. 1, 2000 [doi>10.1006/inco.1999.2846]
• 6: Dov Gabbay , Amir Pnueli , Saharon Shelah , Jonathan Stavi, On the temporal analysis of fairness, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567462]
• 7: T. Hafer , W. Thomas, Computation tree logic CTL^* and path quantifiers in the monadic theory of the binary tree, 14th International Colloquium on Automata, languages and programming, p.269-279, July 1987, Karlsruhe, Germany
• 8: Hans Kamp. Tense logic and the theory of linear order. PhD thesis, University of California, Los Angeles, 1968.
• 9: Leonid Libkin. Elements of Finite Model Theory. Springer, 2004.
• 10: Maarten Marx, Conditional XPath, the first order complete XPath dialect, Proceedings of the twenty-third ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, June 14-16, 2004, Paris, France [doi>10.1145/1055558.1055562]
• 11: Maarten Marx, Conditional XPath, ACM Transactions on Database Systems (TODS), v.30 n.4, p.929-959, December 2005 [doi>10.1145/1114244.1114247]
• 12: Maarten Marx. First Order Paths in Ordered Trees. In ICDT, 2005.
• 13: Maarten Marx and Maarten de Rijke. Semantic Characterizations of XPath. In TDM'04 Workshop on XML Databases and Information Retrieval, 2004.
• 14: Faron Moller , Alexander Rabinovich, On the Expressive Power of CTL, Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, p.360, July 02-05, 1999
• 15: Andreas Potthoff, First-Order Logic on Finite Trees, Proceedings of the 6th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.125-139, May 22-26, 1995
• 16: Alexander Moshe Rabinovich, Expressive Power of Temporal Logics, Proceedings of the 13th International Conference on Concurrency Theory, p.57-75, August 20-23, 2002
• 17: Alexander Rabinovich. Personal communciation, 2008.
• 18: Alexander Moshe Rabinovich , Shahar Maoz, Why so Many Temporal Logics Climb up the Trees?, Proceedings of the 25th International Symposium on Mathematical Foundations of Computer Science, p.629-639, September 01, 2000
• 19: Denis Thérien , Thomas Wilke, Temporal Logic and Semidirect Products: An Effective Characterization of the Until Hierarchy, SIAM Journal on Computing, v.31 n.3, p.777-798, 2001 [doi>10.1137/S0097539797322772]
• 20: World Wide Web Consortium. XML Path Language (XPath) Recommendation. http://www.w3c.org/TR/xpath/, November 1999.