Diego Figueira
ABSTRACT
We 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 constraints is shown here to be decidable.
To show decidability we introduce a model of alternating automata on data trees that can move downwards and rightwards in the tree, have one register for storing data and compare them for equality, and have the ability to (1) non-deterministically guess a data value and store it, and (2) quantify universally over the set of data values seen so far during the run. This model extends the work of Jurdziński and Lazić. Decidability of the finitary non-emptiness problem for this model is obtained by a direct reduction to a well-structured transition system, contrary to previous approaches.
- Michael Benedikt, Wenfei Fan, and Floris Geerts. XPath satisfiability in the presence of DTDs. J. ACM, 55(2), 2008. Google Scholar
Digital Library
- Mikotaj Bojańczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data trees and XML reasoning. In PODS, pages 10--19. ACM Press, 2006. Google ScholarDigital Library
- Balder ten Cate. The expressivity of XPath with transitive closure. In PODS, pages 328--337. ACM Press, 2006. Google ScholarDigital Library
- Balder ten Cate and Luc Segoufin. XPath, transitive closure logic, and nested tree walking automata. In PODS, pages 251--260. ACM Press, 2008. Google ScholarDigital Library
- James Clark and Steve DeRose. XML path language (XPath). Website, November 1999. W3C Recommendation. http://www.w3.org/TR/xpath.Google Scholar
- Stéphane Demri and Ranko Lazić. LTL with the freeze quantifier and register automata. In LICS, pages 17--26. IEEE Computer Society Press, 2006. Google ScholarDigital Library
- Diego Figueira. Satisfiability of downward XPath with data equality tests. In PODS, pages 197--206. ACM Press, 2009. Google ScholarDigital Library
- Diego Figueira and Luc Segoufin. Future-looking logics on data words and trees. In MFCS, volume 5734 of LNCS, pages 331--343. Springer, 2009. Google ScholarDigital Library
- Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1--2):63--92, 2001. Google ScholarDigital Library
- Floris Geerts and Wenfei Fan. Satisfiability of XPath queries with sibling axes. In DBPL, volume 3774 of LNCS, pages 122--137. Springer, 2005. Google ScholarDigital Library
- Georg Gottlob, Christoph Koch, and Reinhard Pichler. Efficient algorithms for processing XPath queries. ACM Trans. Database Syst., 30(2):444--491, 2005. Google ScholarDigital Library
- Marcin Jurdziński and Ranko Lazić. Alternating automata on data trees and XPath satisfiability. CoRR, abs/0805.0330, 2008.Google Scholar
- Maarten Marx. XPath with conditional axis relations. In EDBT, volume 2992 of LNCS, pages 477--494. Springer, 2004.Google Scholar
Index Terms
- Forward-XPath and extended register automata on data-trees
Recommendations
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 ...
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 ...
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 ...
Comments