article

A system for the static analysis of XPath

Authors:

Pierre Genevès,

Nabil LayaïdaAuthors Info & Claims

ACM Transactions on Information Systems (TOIS), Volume 24, Issue 4

Pages 475 - 502

https://doi.org/10.1145/1185877.1185882

Published: 01 October 2006 Publication History

Abstract

XPath is the standard language for navigating XML documents and returning a set of matching nodes. We present a sound and complete decision procedure for containment of XPath queries, as well as other related XPath decision problems such as satisfiability, equivalence, overlap, and coverage. The considered XPath fragment covers most of the language features used in practice. Specifically, we propose a unifying logic for XML, namely, the alternation-free modal μ-calculus with converse. We show how to translate major XML concepts such as XPath and regular XML types (including DTDs) into this logic. Based on these embeddings, we show how XPath decision problems, in the presence or absence of XML types, can be solved using a decision procedure for μ-calculus satisfiability. We provide a complexity analysis of our system together with practical experiments to illustrate the efficiency of the approach for realistic scenarios.

References

[1]

Abiteboul, S. and Vianu, V. 1999. Regular path queries with constraints. J. Compute. Syst. Sci. 58, 3, 428--452.]]

[2]

Afanasiev, L., Blackburn, P., Dimitriou, I., Gaiffe, B., Goris, E., Marx, M., and de Rijke, M. 2005. PDL for ordered trees. J. Appl. Non-Classical Logics 15, 2, 115--135.]]

[3]

Amer-Yahia, S., Cho, S., Lakshmanan, L. V. S., and Srivastava, D. 2001. Minimization of tree pattern queries. SIGMOD Record 30, 2, 497--508.]]

[4]

Arnold, A. and Niwinski, D. 1992. Fixed point characterization of weak monadic logic definable sets of trees. In Tree Automata and Languages. North-Holland, Amsterdam, Netherlands. 159--188.]]

[5]

Baader, F. and Tobies, S. 2001. The inverse method implements the automata approach for modal satisfiability. In IJCAR '01: Proceedings of the 1st International Joint Conference on Automated Reasoning. Springer-Verlag, London. 92--106.]]

[6]

Barceló, P. and Libkin, L. 2005. Temporal logics over unranked trees. In LICS: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, New York. 31--40.]]

[7]

Benedikt, M., Fan, W., and Geerts, F. 2005. XPath satisfiability in the presence of DTDs. In PODS: Proceedings of the 24th ACM Symposium on Principles of Database Systems. ACM, New York. 25--36.]]

[8]

Benedikt, M. and Segoufin, L. 2005. Regular tree languages definable in FO. In STACS: Proceedings of the 22nd Annual Symposium on Theoretical Aspects of Computer Science. Lcture Notes in Computer Science vol. 3404. Springer-Verlag. 327--339.]]

[9]

Berglund, A., Boag, S., Chamberlin, D., Fernández, M. F., Kay, M., Robie, J., and Siméon, J. 2006. XML path language (XPath) 2.0, W3C candidate recommendation. http://www.w3.org/TR/xpath20/.]]

[10]

Bray, T., Paoli, J., Sperberg-McQueen, C. M., Maler, E., and Yergeau, F. 2004. Extensible markup language (XML) 1.0 (3rd ed.), W3C recommendation. http://www.w3.org/TR/2004/REC-xml-20040204/.]]

[11]

Bryant, R. E. 1986. Graph-Based algorithms for Boolean function manipulation. IEEE Trans. Comput. 35, 8, 677--691.]]

[12]

Clark, J. and DeRose, S. 1999. XML path language (XPath) version 1.0, W3C recommendation. http://www.w3.org/TR/1999/REC-xpath-19991116.]]

[13]

Clarke, E. M. and Emerson, E. A. 1981. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Proceedings of the Logic of Programs Workshop. Lecture Notes in Computer Science vol. 131. Springer-Verlag. 52--71.]]

[14]

Deutsch, A. and Tannen, V. 2001. Containment of regular path expressions under integrity constraints. In KRDB: Proceedings of the 8th International Workshop on Knowledge Representation Meets Databases. CEUR Workshop Proceedings vol. 45, 1--11.]]

[15]

Doner, J. 1970. Tree acceptors and some of their applications. J. Comput. Syst. Sci. 4, 406--451.]]

[16]

Edmund, M., Clarke, J., Grumberg, O., and Peled, D. A. 1999. Model Checking. MIT Press, Cambridge, MA.]]

[17]

Fallside, D. C. and Walmsley, P. 2004. XML Schema part 0: Primer 2nd ed., W3C recommendation. http://www.w3.org/TR/xmlschema-0/.]]

[18]

Fan, W., Chan, C.-Y., and Garofalakis, M. 2004. Secure XML querying with security views. In SIGMOD: Proceedings of the ACM SIGMOD International Conference on Management of Data. ACM Press, New York. 587--598.]]

[19]

Fischer, M. J. and Ladner, R. E. 1979. Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18, 2, 194--211.]]

[20]

Franceschet, M. 2005. XPathMark---An XPath benchmark for XMark generated data. In XSYM: Proceedings of the 3rd International Symposium on Database and XML Technologies. Lecture Notes in Computer Science vol. 3671. Springer-Verlag. 129--143.]]

[21]

Genevès, P. and Layaïda, N. 2006. A μ-calculus satisfiability solver for XML. http://wam.inrialpes.fr/xml.]]

[22]

Genevès, P. and Vion-Dury, J.-Y. 2004a. Logic-Based XPath optimization. In DocEng: Proceedings of the ACM Symposium on Document Engineering. ACM Press, New York. 211--219.]]

[23]

Genevès, P. and Vion-Dury, J.-Y. 2004b. XPath formal semantics and beyond: A Coq-Based approach. In TPHOLs: Emerging Trends Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics. Salt Lake City, UT. 181--198.]]

[24]

Gottlob, G., Koch, C., and Pichler, R. 2005. Efficient algorithms for processing XPath queries. ACM Trans. Database Syst. 30, 2, 444--491.]]

[25]

Grädel, E., Thomas, W., and Wilke, T., Eds. 2002. Automata Logics, and Infinite Games: A Guide to Current Research. Springer-Verlag, New York.]]

[26]

Grzegorczyk, A. 1953. Some classes of recursive functions. Rozprawy Matematyczne 4, 1--45.]]

[27]

Hojati, R., Krishnan, S. C., and Brayton, R. K. 1996. Early quantification and partitioned transition relations. In ICCD: Proceedings of the International Conference on Computer Design, VLSI in Computers and Processors. IEEE Computer Society. 12--19.]]

[28]

Hopcroft, J. E., Motwani, R., Rotwani, and Ullman, J. D. 2000. Introduction to Automata Theory, Languages and Computability. Addison-Wesley Longman, Boston.]]

[29]

Hoschka, P. 1998. Synchronized multimedia integration language (SMIL) 1.0 specification, W3C recommendation. http://www.w3.org/TR/REC-smil/.]]

[30]

Hosoya, H., Vouillon, J., and Pierce, B. C. 2005. Regular expression types for XML. ACM Trans. Program. Lang. Syst. 27, 1, 46--90.]]

[31]

Kozen, D. 1983. Results on the propositional μ-calculus. Theoret. Comput. Sci. 27, 333--354.]]

[32]

Kozen, D. 1988. A finite model theorem for the propositional μ-calculus. Studia Logica 47, 3, 233--241.]]

[33]

Kupferman, O. and Vardi, M. 1999. The weakness of self-complementation. In Proceedings of the 16th Symposium on Theoretical Aspects of Computer Science. Lecture Notes in Computer Science vol. 1563. Springer-Verlag. 455--466.]]

[34]

Levin, M. Y. and Pierce, B. C. 2005. Type-Based optimization for regular patterns. In DBPL: Proceedings of the 10th International Symposium on Database Programming Languages. Lecture Notes in Computer Science vol. 3774. Springer-Verlag.]]

[35]

Martens, W. and Neven, F. 2004. Frontiers of tractability for typechecking simple XML transformations. In PODS: Proceedings of the 23rd ACM Symposium on Principles of Database Systems. ACM, New York. 23--34.]]

[36]

Marx, M. 2004a. Conditional XPath, the 1st order complete XPath dialect. In PODS: Proceedings of the 23rd ACM Symposium on Principles of Database Systems. ACM, New York. 13--22.]]

[37]

Marx, M. 2004b. XPath with conditional axis relations. In Proceedings of the 9th International Conference on Extending Database Technology. Lecture Notes in Computer Science vol. 2992. Springer-Verlag. 477--494.]]

[38]

Miklau, G. and Suciu, D. 2004. Containment and equivalence for a fragment of XPath. J. ACM 51, 1, 2--45.]]

[39]

Murata, M., Lee, D., Mani, M., and Kawaguchi, K. 2005. Taxonomy of XML schema languages using formal language theory. ACM Trans. Internet Technol. 5, 4, 660--704.]]

[40]

Neven, F. 2002a. Automata, logic, and XML. In CSL: Proceedings of the 16th International Workshop and 11th Annual Conference of the EACSL on Computer Science Logic. Springer-Verlag. 2--26.]]

[41]

Neven, F. 2002b. Automata theory for XML researchers. SIGMOD Record 31, 3, 39--46.]]

[42]

Neven, F. and Schwentick, T. 2003. XPath containment in the presence of disjunction, DTDs, and variables. In ICDT: Proceedings of the 9th International Conference on Database Theory. Lecture Notes in Computer Science vol. 2572. Springer-Verlag. 315--329.]]

[43]

Pan, G., Sattler, U., and Vardi, M. Y. 2002. BDD-Based decision procedures for K. In CADE: Proceedings of the 18th International Conference on Automated Deduction. Springer-Verlag. 16--30.]]

[44]

Pemberton, S. 2000. XHTML 1.0 the extensible hypertext markup language (2nd ed.), W3C recommendation. http://www.w3.org/TR/xhtml1/.]]

[45]

Schwentick, T. 2004. XPath query containment. SIGMOD Record 33, 1, 101--109.]]

[46]

Sur, G., Hammer, J., and Siméon, J. 2004. Updatex---An XQuery-Based language for processing updates in XML. In PLAN-X: Proceedings of the International Workshop on Programming Language Technologies for XML. Venice, Italy. BRICS Notes Series vol. NS-03-4. BRICS, Aarhus, Denmark. 40--53.]]

[47]

Tanabe, Y., Takahashi, K., Yamamoto, M., Tozawa, A., and Hagiya, M. 2005. A decision procedure for the alternation-free two-way modal μ-calculus. In TABLEAUX: Proceedings of the 14th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science vol. 3702. Springer-Verlag. 277--291.]]

[48]

Thatcher, J. W. and Wright, J. B. 1968. Generalized finite automata theory with an application to a decision problem of second-order logic. Math. Syst. Theory 2, 1, 57--81.]]

[49]

Tozawa, A. 2001. Towards static type checking for XSLT. In DocEng: Proceedings of the ACM Symposium on Document Engineering. ACM, New York. 18--27.]]

[50]

Vardi, M. Y. 1998. Reasoning about the past with two-way automata. In ICALP: Proceedings of the 25th International Colloquium on Automata, Languages and Programming. Springer-Verlag. 628--641.]]

[51]

Wadler, P. 2000. Two semantics for XPath. Internal Tech. Note of the W3C XSL Working Group. http://homepages.inf.ed.ac.uk/wadler/papers/xpath-semantics/xpath-semantics.pdf.]]

[52]

Wood, P. T. 2000. On the equivalence of XML patterns. In CL: Proceedings of the 1st International Conference on Computational Logic. Lecture Notes in Computer Science vol. 1861. Springer-Verlag. 1152--1166.]]

[53]

Wood, P. T. 2003. Containment for XPath fragments under DTD constraints. In ICDT: Proceedings of the 9th International Conference on Database Theory. Lecture Notes in Computer Science vol. 2572. Springer-Verlag. 300--314.]]

Cited By

Spasić MVujošević Janičić M(2023)Solving the SPARQL query containment problem with SpeCSWeb Semantics: Science, Services and Agents on the World Wide Web10.1016/j.websem.2022.10077076:COnline publication date: 1-Apr-2023
https://dl.acm.org/doi/10.1016/j.websem.2022.100770
Fujimoto HSuzuki NKwon Y(2023)Checking Pattern Query Containment Under Shape ExpressionSN Computer Science10.1007/s42979-023-02142-z4:6Online publication date: 12-Oct-2023
https://dl.acm.org/doi/10.1007/s42979-023-02142-z
Mahfoud HDamiani ESilvestri CIvanovic MChbeir RManolopoulos Y(2022)Towards a Strong Containment for Efficient Matching of Expressive Graph PatternsProceedings of the 14th International Conference on Management of Digital EcoSystems10.1145/3508397.3564851(48-55)Online publication date: 19-Oct-2022
https://dl.acm.org/doi/10.1145/3508397.3564851
Show More Cited By

Index Terms

A system for the static analysis of XPath

Recommendations

Logic-based XPath optimization
DocEng '04: Proceedings of the 2004 ACM symposium on Document engineering

XPath [5] was introduced by the W3C as a standard language for specifying node selection, matching conditions, and for computing values from an XML document. XPath is now used in many XML standards such as XSLT [4] and the forthcoming XQuery [10] ...
Deciding XPath containment with MSO

XPath is the standard language for addressing parts of an XML document. We present a sound and complete decision procedure for containment of XPath queries. The considered XPath fragment covers most of the language features used in practice. ...
XPath satisfiability in the presence of DTDs

We study the satisfiability problem associated with XPath in the presence of DTDs. This is the problem of determining, given a query p in an XPath fragment and a DTD D, whether or not there exists an XML document T such that T conforms to D and the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Information Systems

ACM Transactions on Information Systems Volume 24, Issue 4

October 2006

138 pages

ISSN:1046-8188

EISSN:1558-2868

DOI:10.1145/1185877

Issue’s Table of Contents

Copyright © 2006 ACM.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 October 2006

Published in TOIS Volume 24, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

30
Total Citations
View Citations
565
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)2

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Spasić MVujošević Janičić M(2023)Solving the SPARQL query containment problem with SpeCSWeb Semantics: Science, Services and Agents on the World Wide Web10.1016/j.websem.2022.10077076:COnline publication date: 1-Apr-2023
https://dl.acm.org/doi/10.1016/j.websem.2022.100770
Fujimoto HSuzuki NKwon Y(2023)Checking Pattern Query Containment Under Shape ExpressionSN Computer Science10.1007/s42979-023-02142-z4:6Online publication date: 12-Oct-2023
https://dl.acm.org/doi/10.1007/s42979-023-02142-z
Mahfoud HDamiani ESilvestri CIvanovic MChbeir RManolopoulos Y(2022)Towards a Strong Containment for Efficient Matching of Expressive Graph PatternsProceedings of the 14th International Conference on Management of Digital EcoSystems10.1145/3508397.3564851(48-55)Online publication date: 19-Oct-2022
https://dl.acm.org/doi/10.1145/3508397.3564851
Mahfoud H(2021)Conditional Graph Pattern Matching with a Basic Static AnalysisPattern Recognition and Artificial Intelligence10.1007/978-3-030-71804-6_22(298-313)Online publication date: 18-Mar-2021
https://doi.org/10.1007/978-3-030-71804-6_22
Spasic MJanicic M(2020)SpeCS — SPARQL Query Containment Solver2020 Zooming Innovation in Consumer Technologies Conference (ZINC)10.1109/ZINC50678.2020.9161435(31-35)Online publication date: May-2020
https://doi.org/10.1109/ZINC50678.2020.9161435
Taktek EThakker D(2020)Pentagonal scheme for dynamic XML prefix labellingKnowledge-Based Systems10.1016/j.knosys.2020.106446(106446)Online publication date: Sep-2020
https://doi.org/10.1016/j.knosys.2020.106446
Hague MLin AHong C(2019)CSS Minification via Constraint SolvingACM Transactions on Programming Languages and Systems10.1145/331033741:2(1-76)Online publication date: 19-Jun-2019
https://dl.acm.org/doi/10.1145/3310337
Chekol MEuzenat JGenevès PLayaïda N(2018)SPARQL Query Containment Under SchemaJournal on Data Semantics10.1007/s13740-018-0087-17:3(133-154)Online publication date: 22-May-2018
https://doi.org/10.1007/s13740-018-0087-1
Abbas AGenevès PRoisin CLayaïda N(2017)SPARQL Query Containment with ShEx ConstraintsAdvances in Databases and Information Systems10.1007/978-3-319-66917-5_23(343-356)Online publication date: 25-Aug-2017
https://doi.org/10.1007/978-3-319-66917-5_23
Almendros-Jiménez JBecerra-Terón A(2017)Automatic property-based testing and path validation of XQuery programsSoftware Testing, Verification and Reliability10.1002/stvr.162527:1-2(e1625)Online publication date: 6-Feb-2017
https://doi.org/10.1002/stvr.1625
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents