Diego Figueira
Abstract
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 also hold when path expressions allow closure under the Kleene star operator. To obtain these results, we introduce a Downward Data automata model (DD automata) over trees with data, which has a decidable emptiness problem. Satisfiability of downward-XPath can be reduced to the emptiness problem of DD automata and hence its decidability follows. Although downward-XPath does not include any horizontal axis, DD automata are more expressive and can perform some horizontal tests. Thus, we show that the satisfiability remains in EXPTIME even in the presence of the regular constraints expressible by DD automata. However, the same problem in the presence of any regular constraint is known to have a nonprimitive recursive complexity. Finally, we give the exact complexity of the satisfiability problem for several fragments of downward-XPath.
Supplemental Material
Available for Download
The proof is given in an electronic appendix, available online in the ACM Digital Library.
- Benedikt, M., Fan, W., and Geerts, F. 2008. XPath satisfiability in the presence of DTDs. J. ACM 55, 2, 1--79. Google Scholar
Digital Library
- Blackburn, P., De Rijke, M., and Venema, Y. 2001. Modal Logic. Cambridge University Press. Google ScholarDigital Library
- Bojańczyk, M., Muscholl, A., Schwentick, T., and Segoufin, L. 2009. Two-variable logic on data trees and XML reasoning. J. ACM 56, 3, 1--48. Google ScholarDigital Library
- Ceri, S., Gottlob, G., and Tanca, L. 1989. What you always wanted to know about datalog (and never dared to ask). IEEE Trans. Knowl. Data Engin. 1, 1, 146--166. Google ScholarDigital Library
- Clark, J. and DeRose, S. 1999. XML path language (XPath). Website. W3C Recommendation. http://www.w3.org/TR/xpath.Google Scholar
- Demri, S. and Lazić, R. 2009. LTL with the freeze quantifier and register automata. ACM Trans. Comput. Logic 10, 3. Google ScholarDigital Library
- Fan, W., Chan, C. Y., and Garofalakis, M. N. 2004. Secure XML querying with security views. In Proceedings of the ACM SIGACT-SIGMOD-SIGART International Conference on Management of Data (SIGMOD’04). ACM Press, 587--598. Google ScholarDigital Library
- Figueira, D. 2009. Satisfiability of downward XPath with data equality tests. In Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS’09). ACM Press, 197--206. Google ScholarDigital Library
- Figueira, D. 2010a. Forward-XPath and extended register automata on data-trees. In Proceedings of the International Conference on Database Theory (ICDT’10). ACM Press, 230--240. Google ScholarDigital Library
- Figueira, D. 2010b. Reasoning on words and trees with data. Ph.D. thesis, Laboratoire Spécification et Vérification, ENS Cachan, France.Google Scholar
- Figueira, D. 2011. A decidable two-way logic on data words. In Proceedings of the Annual IEEE Symposium on Logic in Computer Science (LICS’11). IEEE Computer Society Press. Google ScholarDigital Library
- Figueira, D. and Segoufin, L. 2009. Future-looking logics on data words and trees. In Proceedings of the International Symposium on Mathematical Foundations of Computer Science (MFCS’09). Lecture Notes in Computer Science, vol. 5734, Springer, 331--343. Google ScholarDigital Library
- Figueira, D. and Segoufin, L. 2011. Bottom-up automata on data trees and vertical XPath. In Proceedings of the International Symposium on Theoretical Aspects of Computer Science (STACS’11). Springer, 93--104.Google Scholar
- Garey, M. and Johnson, D. 1979. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman. Google ScholarDigital Library
- Geerts, F. and Fan, W. 2005. Satisfiability of XPath queries with sibling axes. In Proceedings of the International Symposium on Database Programming Languages (DBPL’05). Lecture Notes in Computer Science, vol. 3774, Springer, 122--137. Google ScholarDigital Library
- Gottlob, G., Koch, C., and Pichler, R. 2002. Efficient algorithms for processing xpath queries. In Proceedings of the 28th International Conference on Very Large Data Bases (VLDB’02). VLDB Endowment, 95--106. Google ScholarDigital Library
- Gottlob, G., Koch, C., and Pichler, R. 2005. Efficient algorithms for processing XPath queries. ACM Trans. Datab. Syst. 30, 2, 444--491. Google ScholarDigital Library
- Jurdziński, M. and Lazić, R. 2008. Alternating automata on data trees and XPath satisfiability. Computing Research Repository (CoRR).Google Scholar
- Ladner, R. E. 1977. The computational complexity of provability in systems of modal propositional logic. SIAM J. Comput. 6, 3, 467--480.Google ScholarDigital Library
- Martens, W. and Neven, F. 2007. Frontiers of tractability for typechecking simple xml transformations. J. Comput. Syst. Sci. 73, 3, 362--390. Google ScholarDigital Library
- Marx, M. 2004. XPath with conditional axis relations. In Proceedings of the International Conference on Extending Database Technology (EDBT’04). Lecture Notes in Computer Science, vol. 2992, Springer, 477--494.Google ScholarCross Ref
- Marx, M. 2005. First order paths in ordered trees. In Proceedings of the International Conference on Database Theory (ICDT’05). Springer, 114--128. Google ScholarDigital Library
- Schnoebelen, P. 2002. Verifying lossy channel systems has nonprimitive recursive complexity. Inf. Process. Lett. 83, 5, 251--261. Google ScholarDigital Library
- ten Cate, B. 2006. The expressivity of XPath with transitive closure. In Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS’06). ACM Press, 328--337. Google ScholarDigital Library
- ten Cate, B. and Segoufin, L. 2008. XPath, transitive closure logic, and nested tree walking automata. In Proceedings of the ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS’08). ACM Press, 251--260. Google ScholarDigital Library
Index Terms
- Decidability of Downward XPath
Recommendations
On XPath with transitive axes and data tests
PODS '13: Proceedings of the 32nd ACM SIGMOD-SIGACT-SIGAI symposium on Principles of database systemsWe study the satisfiability problem for XPath with data equality tests. XPath is a node selecting language for XML documents whose satisfiability problem is known to be undecidable, even for very simple fragments. However, we show that the ...
Satisfiability of downward XPath with data equality tests
PODS '09: Proceedings of the twenty-eighth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systemsIn this work we investigate the satisfiability problem for the logic XPath(↓*, ↓,=), that includes all downward axes as well as equality and inequality tests. We address this problem in the absence of DTDs and the sibling axis. We prove that this ...
Forward-XPath and extended register automata on data-trees
ICDT '10: Proceedings of the 13th International Conference on Database TheoryWe consider a fragment of XPath named 'forward-XPath', which contains all descendant and rightwards sibling axes as well as data equality and inequality tests. The satisfiability problem for forward-XPath in the presence of DTDs and even of primary key ...
Comments