More Web Proxy on the site http://driver.im/

article

Efficient static analysis of XML paths and types

Authors:

Pierre Genevès,

Nabil Layaïda,

Alan SchmittAuthors Info & Claims

ACM SIGPLAN Notices, Volume 42, Issue 6

Pages 342 - 351

https://doi.org/10.1145/1273442.1250773

Published: 10 June 2007 Publication History

Abstract

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 μ-calculus without greatest fixpoint, restricted to finite trees, and where formulas are cycle-free.

Our proof method is based on two auxiliary results. First, XML regular tree types and XPath expressions have a linear translation to cycle-free formulas. Second, the least and greatest fixpoints are equivalent for finite trees, hence the logic is closed under negation.

Building on these results, we describe a practical, effective system for solving the satisfiability of a formula. The system has been experimented with some decision problems such as XPath emptiness, containment, overlap, and coverage, with or without type constraints. The benefit of the approach is that our system can be effectively used in static analyzers for programming languages manipulating both XPath expressions and XML type annotations (as input and output types).

References

[1]

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.

[2]

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.

Digital Library

[3]

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.

Digital Library

[4]

V. Benzaken, G. Castagna, and A. Frisch. CDuce: An XML-centric general-purpose language. In ICFP '03: Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, pages 51--63, New York, NY, USA, 2003. ACM Press.

Digital Library

[5]

R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Trans. on Computers, 35(8):677--691, 1986.

Digital Library

[6]

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.

[7]

D. Colazzo, G. Ghelli, P. Manghi, and C. Sartiani. Static analysis for path correctness of XML queries. J. Funct. Program., 16(4-5):621--661, 2006.

Digital Library

[8]

S. Dal Zilio, D. Lugiez, and C. Meyssonnier. A logic you can count on. In POPL '04: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 135--146, New York, NY, USA, 2004. ACM Press.

Digital Library

[9]

J. Doner. Tree acceptors and some of their applications. Journal of Computer and System Sciences, 4:406--451, 1970.

Digital Library

[10]

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

Digital Library

[11]

E. A. Emerson and C. S. Jutla. Tree automata, μ-calculus and determinacy. In Proceedings of the 32nd annual Symposium on Foundations of Computer Science, pages 368--377, Los Alamitos, CA, USA, 1991. IEEE Computer Society Press.

Digital Library

[12]

W. Fan, C.-Y. Chan, and 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.

Digital Library

[13]

V. Gapeyev and B.C. Pierce. Regular object types. In European Conference on Object-Oriented Programming (ECOOP), Darmstadt, Germany, 2003. A preliminary version was presented at FOOL '03.

[14]

P. Genevès and N. Layaïda. A system for the static analysis of XPath. ACM Trans. Inf. Syst., 24(4):475--502, 2006.

Digital Library

[15]

P. Genevès and N. Layaïda. Deciding XPath containement with MSO. Data & Knowledge Engineering, to appear, 2007.

Digital Library

[16]

P. Genevès, N. Layaïda, and A. Schmitt. A satisfiability solver for XML and XPath, June 2006. http://wam.inrialpes.fr/xml.

[17]

P. Genevès and J.-Y. Vion-Dury. Logic-based XPath optimization. In DocEng '04: Proceedings of the 2004 ACM Symposium on Document Engineering, pages 211--219, NY, USA, 2004. ACM Press.

Digital Library

[18]

E. Grädel, W. Thomas, and T. Wilke, editors. Automata logics, and infinite games: a guide to current research. Springer-Verlag, New York, NY, USA, 2002.

[19]

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

Digital Library

[20]

G. P. Huet. The zipper. J. Funct. Program., 7(5):549--554, 1997.

Digital Library

[21]

N. Klarlund, A. Møller, and M. I. Schwartzbach. MONA 1.4, January 2001. http://www.brics.dk/mona/.

[22]

D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333--354, 1983.

[23]

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 LNCS, London, UK, August 2005. Springer-Verlag.

Digital Library

[24]

G. Miklau and D. Suciu. Containment and equivalence for a fragment of XPath. Journal of the ACM, 51(1):2--45, 2004.

Digital Library

[25]

A. Møller and M. I. Schwartzbach. The design space of type checkers for XML transformation languages. In Proc. Tenth International Conference on Database Theory, ICDT '05, volume 3363 of LNCS, pages 17--36. Springer-Verlag, January 2005.

Digital Library

[26]

M. Murata, D. Lee, M. Mani, and K. Kawaguchi. Taxonomy of XML schema languages using formal language theory. ACM Transactions on Internet Technology, 5(4):660--704, 2005.

Digital Library

[27]

G. Pan, U. Sattler, and M. Y. Vardi. BDD-based decision procedures for the modal logic K. Journal of Applied Non-classical Logics, 16(1-2):169--208, 2006.

[28]

T. Schwentick. XPath query containment. SIGMOD Record, 33(1):101--109, 2004.

Digital Library

[29]

Y. Tanabe, K. Takahashi, M. Yamamoto, A. Tozawa, and M. Hagiya. A decision procedure for the alternation-free two-way modal μcalculus. In In TABLEAUX 2005, volume 3702 of LNCS, pages 277--291, London, UK, September 2005. Springer-Verlag.

Digital Library

[30]

A. Tozawa. On binary tree logic for XML and its satisfiability test. In PPL '04: Informal Proceedings of the Sixth JSSST Workshop on Programming and Programming Languages, 2004.

[31]

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.

Digital Library

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
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
Saleem MStadler CMehmood QLehmann JNgomo A(2017)SQCFrameworkProceedings of the 9th Knowledge Capture Conference10.1145/3148011.3148017(1-8)Online publication date: 4-Dec-2017
https://dl.acm.org/doi/10.1145/3148011.3148017
Show More Cited By

Index Terms

Efficient static analysis of XML paths and types

Recommendations

Efficient static analysis of XML paths and types
PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation

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 ...
Decidability of Downward XPath

We investigate the satisfiability problem for downward-XPath, the fragment of XPath that includes the child and descendant axes, and tests for (in)equality of attributes’ values. We prove that this problem is decidable, EXPTIME-complete. These bounds ...
Type checking and inference for polymorphic and existential types
CATS '09: Proceedings of the Fifteenth Australasian Symposium on Computing: The Australasian Theory - Volume 94

This paper proves undecidability of type checking and type inference problems in some variants of typed lambda calculi with polymorphic and existential types. First, type inference in the domain-free polymorphic lambda calculus is proved to be ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 42, Issue 6

Proceedings of the 2007 PLDI conference

June 2007

491 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1273442

Issue’s Table of Contents

PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation
June 2007
508 pages
ISBN:9781595936332
DOI:10.1145/1250734
General Chair:
Jeanne Ferrante
University of California, San Diego, USA
,
Program Chair:
Kathryn S. McKinley
University of Texas at Austin, USA

Copyright © 2007 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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 10 June 2007

Published in SIGPLAN Volume 42, Issue 6

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

54
Total Citations
View Citations
603
Total Downloads

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

Reflects downloads up to 31 Dec 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
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
Saleem MStadler CMehmood QLehmann JNgomo A(2017)SQCFrameworkProceedings of the 9th Knowledge Capture Conference10.1145/3148011.3148017(1-8)Online publication date: 4-Dec-2017
https://dl.acm.org/doi/10.1145/3148011.3148017
Chekol MPirrò G(2016)Containment of Expressive SPARQL Navigational QueriesThe Semantic Web – ISWC 201610.1007/978-3-319-46523-4_6(86-101)Online publication date: 23-Sep-2016
https://doi.org/10.1007/978-3-319-46523-4_6
Wudage Chekol MEuzenat JGenevès PLayaïda N(2013)Evaluating and Benchmarking SPARQL Query Containment SolversProceedings of the 12th International Semantic Web Conference - Part II10.1007/978-3-642-41338-4_26(408-423)Online publication date: 21-Oct-2013
https://dl.acm.org/doi/10.1007/978-3-642-41338-4_26
Oliveira RGenevès PLayaïda NConcolato CSchmitz P(2012)Toward automated schema-directed code revisionProceedings of the 2012 ACM symposium on Document engineering10.1145/2361354.2361377(103-106)Online publication date: 4-Sep-2012
https://dl.acm.org/doi/10.1145/2361354.2361377
Limón YBárcenas EBenítez-Guerrero ECastillo GVelázquez-Mena A(2020)Mu-Calculus Satisfiability with Arithmetic ConstraintsProgramming and Computer Software10.1134/S036176882008013746:8(503-510)Online publication date: 22-Dec-2020
https://doi.org/10.1134/S0361768820080137
Im HGenevès PGesbert NLayaïda N(2020)Backward type inference for XML queriesTheoretical Computer Science10.1016/j.tcs.2020.03.020Online publication date: Mar-2020
https://doi.org/10.1016/j.tcs.2020.03.020
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
Chekol MPirrò G(2016)Containment of Expressive SPARQL Navigational QueriesThe Semantic Web – ISWC 201610.1007/978-3-319-46523-4_6(86-101)Online publication date: 23-Sep-2016
https://doi.org/10.1007/978-3-319-46523-4_6
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 Publication

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