Comparing XML path expressions
Pages 65 - 74
Abstract
XPath is the standard declarative language for navigating XML data and returning a set of matching nodes. In the context of XSLT/XQuery analysis, query optimization, and XML type checking, XPath decision problems arise naturally. They notably include XPath comparisons such as equivalence (whether two queries always return the same result), and containment (whether for any tree the result of a particular query is included in the result of a second one).XPath decision problems have attracted a lot of research attention, especially for studying the computational complexity of various XPath fragments. However, what is missing at present is the constructive use of an expressive logic which would allow capturing these decision problems, while providing practically effective decision procedures.In this paper, we propose a logic-based framework for the static analysis of XPath. Specifically, we propose the alternation free modal μ-calculus with converse as the appropriate logic for effectively solving XPath decision problems. We present a translation of a large XPath fragment into μ-calculus, together with practical experiments on the containment using a state-of-the-art EXPTIME decision procedure for μ-calculus satisfiability. These preliminary experiments shed light, for the first time, on the cost of checking the containment in practice. We believe they reveal encouraging results for further static analysis of XML transformations.
References
[1]
S. Abiteboul and V. Vianu. Regular path queries with constraints. Journal of Computer and System Sciences, 58(3):428--452, 1999.]]
[2]
L. Afanasiev, P. Blackburn, I. Dimitriou, B. Gaiffe, E. Goris, M. Marx, and M. de Rijke. PDL for ordered trees. Journal of Applied Non-Classical Logics, 15(2):115--135, 2005.]]
[3]
S. Amer-Yahia, S. Cho, L.V.S. Lakshmanan, and D. Srivastava. Minimization of tree pattern queries. SIGMOD Record, 30(2):497--508, 2001.]]
[4]
A. Arnold and D. Niwinski. Fixed point characterization of weak monadic logic definable sets of trees. In Tree Automata and Languages, pages 159--188. North-Holland, Amsterdam, Netherlands, 1992.]]
[5]
P. Barceló and L. Libkin. Temporal logics over unranked trees. In LICS '05: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, pages 31--40, New York, NY, USA, 2005. IEEE Computer Society.]]
[6]
M. Benedikt, W. Fan, and F. Geerts. XPath satisfiability in the presence of DTDs. In PODS '05: Proceedings of the twenty-fourth ACM Symposium on Principles of Database Systems, pages 25--36, New York, NY, USA, 2005. ACM Press.]]
[7]
M. Benedikt, W. Fan, and G.M. Kuper. Structural properties of XPath fragments. Theoretical Computer Science, 336(1):3--31, 2005.]]
[8]
M. Benedikt and L. Segoufin. Regular tree languages definable in FO. In STACS '05: Proceedings of the 22nd Annual Symposium on Theoretical Aspects of Computer Science, volume 3404 of LNCS, pages 327--339, London, UK, 2005. Springer-Verlag.]]
[9]
J. Clark and S. DeRose. XML path language (XPath) version 1.0, W3C recommendation, November 1999. http://www.w3.org/TR/1999/REC-xpath-19991116.]]
[10]
E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Logic of Programs, Workshop, volume 131 of LNCS, pages 52--71, London, UK, 1981. Springer-Verlag.]]
[11]
A. Deutsch and V. Tannen. Containment of regular path expressions under integrity constraints. In KRDB '01: Proceedings of the 8th International Workshop on Knowledge Representation meets Databases, volume 45 of CEUR Workshop Proceedings, pages 1--11, ceur-ws.org, 2001. CEUR.]]
[12]
J. Doner. Tree acceptors and some of their applications. Journal of Computer and System Sciences, 4:406--451, 1970.]]
[13]
D. Draper, P. Fankhauser, M. Fernández, A. Malhotra, K. Rose, M. Rys, J. Siméon, and P. Wadler. XQuery 1.0 and XPath 2.0 formal semantics, W3C working draft, September 2005. http://www.w3.org/TR/2005/WD-xquery-semantics-20050915/.]]
[14]
W. Fan, C.-Y. Chan, and M. Garofalakis. Secure XML querying with security views. In SIGMOD '04: Proceedings of the 2004 ACM SIGMOD International Conference on Management of Data, pages 587--598, New York, NY, USA, 2004. ACM Press.]]
[15]
M.J. Fischer and R.E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18(2):194--211, 1979.]]
[16]
M. Franceschet. XPathMark - an XPath benchmark for XMark generated data. In XSYM '05: Proceedings of The Third International Symposium on Database and XML Technologies, volume 3671 of LNCS, pages 129--143, London, UK, 2005. Springer-Verlag.]]
[17]
G. Gottlob and C. Koch. Monadic datalog and the expressive power of languages for web information extraction. In PODS '02: Proceedings of the twenty-first ACM Symposium on Principles of Database Systems, pages 17--28, New York, NY, USA, 2002. ACM Press.]]
[18]
G. Gottlob and C. Koch. Monadic queries over tree-structured data. In LICS '02: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, pages 189--202, Washington, DC, USA, 2002. IEEE Computer Society.]]
[19]
G. Gottlob, C. Koch, and R. Pichler. Efficient algorithms for processing xpath queries. ACM Transactions on Database Systems, 30(2):444--491, 2005.]]
[20]
A. Grzegorczyk. Some classes of recursive functions. Rozprawy Matematyczne, 4:1--45, 1953.]]
[21]
D. Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333--354, 1983.]]
[22]
D. Kozen. A finite model theorem for the propositional mu-calculus. Studia Logica, 47(3):233--241, 1988.]]
[23]
O. Kupferman and M. Vardi. The weakness of self-complementation. In Proc. 16th Symp. on Theoretical Aspects of Computer Science, volume 1563 of LNCS, pages 455--466, London, UK, 1999. Springer-Verlag.]]
[24]
M.Y. Levin and B.C. Pierce. Type-based optimization for regular patterns. In DBPL '05: Proceedings of the 10th International Symposium on Database Programming Languages, volume 3774 of Lecture Notes in Computer Science, London, UK, August 2005. Springer-Verlag.]]
[25]
W. Martens and F. Neven. Frontiers of tractability for typechecking simple XML transformations. In PODS '04: Proceedings of the twenty-third ACM Symposium on Principles of Database Systems, pages 23--34, New York, NY, USA, 2004. ACM Press.]]
[26]
M. Marx. Conditional XPath, the first order complete XPath dialect. In PODS '04: Proceedings of the twenty-third ACM Symposium on Principles of Database Systems, pages 13--22, New York, NY, USA, 2004. ACM Press.]]
[27]
M. Marx. XPath with conditional axis relations. In Proceedings of the 9th International Conference on Extending Database Technology, volume 2992 of LNCS, pages 477--494, London, UK, January 2004. Springer-Verlag.]]
[28]
R. Mateescu. Local model-checking of modal mu-calculus on acyclic labeled transition systems. In TACAS '02: Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 281--295, London, UK, 2002. Springer-Verlag.]]
[29]
G. Miklau and D. Suciu. Containment and equivalence for a fragment of XPath. Journal of the ACM, 51(1):2--45, 2004.]]
[30]
F. Neven. Automata theory for XML researchers. SIGMOD Record, 31(3):39--46, 2002.]]
[31]
F. Neven and T. Schwentick. XPath containment in the presence of disjunction, DTDs, and variables. In ICDT '03: Proceedings of the 9th International Conference on Database Theory, volume 2572 of LNCS, pages 315--329, London, UK, 2003. Springer-Verlag.]]
[32]
T. Schwentick. XPath query containment. SIGMOD Record, 33(1):101--109, 2004.]]
[33]
G. Sur, J. Hammer, and J. Siméon. Updatex - an XQuery-based language for processing updates in XML. In PLAN-X 2004: Proceedings of the International Workshop on Programming Language Technologies for XML, Venice, Italy, volume NS-03-4 of BRICS Notes Series, pages 40--53, Aarhus, Denmark, January 2004. BRICS.]]
[34]
Y. Tanabe, K. Takahashi, M. Yamamoto, A. Tozawa, and M. Hagiya. A decision procedure for the alternation-free two-way modal μ-calculus. In TABLEAUX '05: Proceedings of the 14th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, volume 3702 of LNCS, pages 277--291, London, UK, September 2005. Springer-Verlag.]]
[35]
J.W. Thatcher and J.B. Wright. Generalized finite automata theory with an application to a decision problem of second-order logic. Mathematical Systems Theory, 2(1):57--81, 1968.]]
[36]
A. Tozawa. Towards static type checking for XSLT. In DocEng '01: Proceedings of the 2001 ACM Symposium on Document Engineering, pages 18--27, New York, NY, USA, 2001. ACM Press.]]
[37]
M.Y. Vardi. Reasoning about the past with two-way automata. In ICALP '98: Proceedings of the 25th International Colloquium on Automata, Languages and Programming, pages 628--641, London, UK, 1998. Springer-Verlag.]]
[38]
P. Wadler. Two semantics for XPath. Internal Technical Note of the W3C XSL Working Group, http://homepages.inf.ed.ac.uk/wadler/papers/xpathsemantics/xpath-semantics.pdf, January 2000.]]
[39]
P.T. Wood. On the equivalence of XML patterns. In CL '00: Proceedings of the First International Conference on Computational Logic, volume 1861 of LNCS, pages 1152--1166, London, UK, 2000. Springer-Verlag.]]
[40]
P.T. Wood. Containment for XPath fragments under DTD constraints. In ICDT '03: Proceedings of the 9th International Conference on Database Theory, volume 2572 of LNCS, pages 300--314, London, UK, August 2003. Springer-Verlag.]]
Recommendations
Filtering XPath expressions for XML access control
XPath is a standard for specifying parts of XML documents and a suitable language for both query processing and access control of XML. In this paper, we use the XPath expression for representing user queries and access control for XML. And we propose an ...
The essence of XML
The World-Wide Web Consortium (W3C) promotes XML and related standards, including XML Schema, XQuery, and XPath. This paper describes a formalization of XML Schema. A formal semantics based on these ideas is part of the official XQuery and XPath ...
Querying xml documents in logic programming*
Extensible Markup Language (XML) is a simple, very flexible text format derived from SGML. Originally designed to meet the challenges of large-scale electronic publishing, XML is also playing an increasingly important role in the exchange of a wide ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
October 2006
232 pages
Copyright © 2006 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 10 October 2006
Check for updates
Author Tags
Qualifiers
- Article
Conference
Acceptance Rates
Overall Acceptance Rate 194 of 564 submissions, 34%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 261Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 16 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in