Efficient static analysis of XML paths and types

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: Pablo Barcelo, Temporal Logics over Unranked Trees, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), p.31-40, June 26-29, 2005 [doi>10.1109/LICS.2005.51]
• 3: Michael Benedikt , Wenfei Fan , Floris Geerts, XPath satisfiability in the presence of DTDs, Proceedings of the twenty-fourth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, June 13-15, 2005, Baltimore, Maryland [doi>10.1145/1065167.1065172]
• 4: Véronique Benzaken , Giuseppe Castagna , Alain Frisch, CDuce: an XML-centric general-purpose language, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.51-63, August 25-29, 2003, Uppsala, Sweden
• 5: Randal E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation, IEEE Transactions on Computers, v.35 n.8, p.677-691, August 1986 [doi>10.1109/TC.1986.1676819]
• 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: Dario Colazzo , Giorgio Ghelli , Paolo Manghi , Carlo Sartiani, Static analysis for path correctness of XML queries, Journal of Functional Programming, v.16 n.4-5, p.621-661, July 2006 [doi>10.1017/S0956796806005983]
• 8: Silvano Dal Zilio , Denis Lugiez , Charles Meyssonnier, A logic you can count on, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.135-146, January 14-16, 2004, Venice, Italy
• 9: J. Doner. Tree acceptors and some of their applications. Journal of Computer and System Sciences, 4:406--451, 1970.
• 10: Edmund M. Clarke, Jr. , Orna Grumberg , Doron A. Peled, Model checking, MIT Press, Cambridge, MA, 2000
• 11: E. A. Emerson , C. S. Jutla, Tree automata, Mu-Calculus and determinacy, Proceedings of the 32nd annual symposium on Foundations of computer science, p.368-377, September 1991, San Juan, Puerto Rico [doi>10.1109/SFCS.1991.185392]
• 12: Wenfei Fan , Chee-Yong Chan , Minos Garofalakis, Secure XML querying with security views, Proceedings of the 2004 ACM SIGMOD international conference on Management of data, June 13-18, 2004, Paris, France [doi>10.1145/1007568.1007634]
• 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: Pierre Genevès , Nabil Layaïda, A system for the static analysis of XPath, ACM Transactions on Information Systems (TOIS), v.24 n.4, p.475-502, October 2006 [doi>10.1145/1185877.1185882]
• 15: Pierre Genevès , Nabil Layaïda, Deciding XPath containment with MSO, Data & Knowledge Engineering, v.63 n.1, p.108-136, October, 2007 [doi>10.1016/j.datak.2006.11.003]
• 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: Pierre Genevès , Jean-Yves Vion-Dury, Logic-based XPath optimization, Proceedings of the 2004 ACM symposium on Document engineering, October 28-30, 2004, Milwaukee, Wisconsin, USA [doi>10.1145/1030397.1030437]
• 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: Haruo Hosoya , Jérôme Vouillon , Benjamin C. Pierce, Regular expression types for XML, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.1, p.46-90, January 2005 [doi>10.1145/1053468.1053470]
• 20: Gérard Huet, The Zipper, Journal of Functional Programming, v.7 n.5, p.549-554, September 1997 [doi>10.1017/S0956796897002864]
• 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.
• 24: Gerome Miklau , Dan Suciu, Containment and equivalence for a fragment of XPath, Journal of the ACM (JACM), v.51 n.1, p.2-45, January 2004 [doi>10.1145/962446.962448]
• 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.
• 26: Makoto Murata , Dongwon Lee , Murali Mani , Kohsuke Kawaguchi, Taxonomy of XML schema languages using formal language theory, ACM Transactions on Internet Technology (TOIT), v.5 n.4, p.660-704, November 2005 [doi>10.1145/1111627.1111631]
• 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: Thomas Schwentick, XPath query containment, ACM SIGMOD Record, v.33 n.1, March 2004 [doi>10.1145/974121.974140]
• 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.
• 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: Moshe Y. Vardi, Reasoning about The Past with Two-Way Automata, Proceedings of the 25th International Colloquium on Automata, Languages and Programming, p.628-641, July 13-17, 1998

INDEX TERMS

Primary Classification:
  E. Data
  E.1 DATA STRUCTURES
      Subjects: Trees

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Modal logic

General Terms:
Algorithms, Languages, Theory, Verification

Keywords:
XPath, modal logic, satisfiability, type checking