Two-variable logic on data trees and XML reasoning

ABSTRACT

Motivated by reasoning tasks for XML languages, the satisfiability problem of logics on data trees is investigated. The nodes of a data tree have a label from a finite set and a data value from a possibly infinite set. It is shown that satisfiability for two-variable first-order logic is decidable if the tree structure can be accessed only through the child and the next sibling predicates and the access to data values is restricted to equality tests. From this main result, decidability of satisfiability and containment for a data-aware fragment of XPath and of the implication problem for unary key and inclusion constraints is concluded.

REFERENCES

• 1: Noga Alon , Tova Milo , Frank Neven , Dan Suciu , Victor Vianu, XML with data values: typechecking revisited, Journal of Computer and System Sciences, v.66 n.4, p.688-727, 1 June 2003 [doi>10.1016/S0022-0000(03)00032-1]
• 2: Arenas, M., Fan, W., and Libkin, L. 2005. Consistency of XML specifications. In Inconsistency Tolerance. Lecture Notes in Computer Science, vol. 3300. Springer-Verlag, New York, pp. 15--41.
• 3: Michael Benedikt , Christoph Koch, XPath leashed, ACM Computing Surveys (CSUR), v.41 n.1, p.1-54, December 2008 [doi>10.1145/1456650.1456653]
• 4: 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]
• 5: Mikolaj Bojanczyk , Anca Muscholl , Thomas Schwentick , Luc Segoufin , Claire David, Two-Variable Logic on Words with Data, Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, p.7-16, August 12-15, 2006 [doi>10.1109/LICS.2006.51]
• 6: Patricia Bouyer , Antoine Petit , Denis Thérien, An algebraic approach to data languages and timed languages, Information and Computation, v.182 n.2, p.137-162, 01 May 2003 [doi>10.1016/S0890-5401(03)00038-5]
• 7: Brüggemann-Klein, A., Wood, D., and Murata, M. 2001. Regular tree and regular hedge languages over unranked alphabets. Technical report, April. http://citeseer.ist.psu.edu/451005.html.
• 8: Peter Buneman , Susan Davidson , Wenfei Fan , Carmem Hara , Wang-Chiew Tan, Reasoning about keys for XML, Information Systems, v.28 n.8, p.1037-1063, December 2003 [doi>10.1016/S0306-4379(03)00028-0]
• 9: Carme, J., Niehren, J., and Tommasi, M. 2004. Querying unranked trees with stepwise tree automata. In RTA'04. Lecture Notes in Computer Science, vol. 3091. Springer-Verlag, New York, 105--118.
• 10: Cristau, J., Löding, C., and Thomas, W. 2005. Deterministic automata on unranked trees. In FCT'05. Lecture Notes in Computer Science, vol. 3623. Springer-Verlag, New York, pp. 68--79.
• 11: David, C. 2004. Mots et données infinis. Master thesis, Université Paris 7, LIAFA.
• 12: Philippe de Groote , Bruno Guillaume , Sylvain Salvati, Vector Addition Tree Automata, Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, p.64-73, July 13-17, 2004 [doi>10.1109/LICS.2004.51]
• 13: Stephane Demri , Ranko Lazic , David Nowak, On the Freeze Quantifier in Constraint LTL: Decidability and Complexity, Proceedings of the 12th International Symposium on Temporal Representation and Reasoning, p.113-121, June 23-25, 2005 [doi>10.1109/TIME.2005.28]
• 14: Stephane Demri , Ranko Lazic, LTL with the Freeze Quantifier and Register Automata, Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, p.17-26, August 12-15, 2006 [doi>10.1109/LICS.2006.31]
• 15: Kousha Etessami , Moshe Y. Vardi , Thomas Wilke, First-order logic with two variables and unary temporal logic, Information and Computation, v.179 n.2, p.279-295, December 15, 2002 [doi>10.1006/inco.2001.2953]
• 16: Wenfei Fan , Leonid Libkin, On XML integrity constraints in the presence of DTDs, Journal of the ACM (JACM), v.49 n.3, p.368-406, May 2002 [doi>10.1145/567112.567117]
• 17: Geerts, F., and Fan, W. 2005. Satisfiability of XPath queries with sibling axes. In DBPL'05. Lecture Notes in Computer Science, vol. 3774. Springer-Verlag, New York, 122--137.
• 18: Georg Gottlob , Christoph Koch , Reinhard Pichler, Efficient algorithms for processing XPath queries, Proceedings of the 28th international conference on Very Large Data Bases, p.95-106, August 20-23, 2002, Hong Kong, China
• 19: Erich Grädel , Martin Otto, On logics with two variables, Theoretical Computer Science, v.224 n.1-2, p.73-113, Aug. 6, 1999 [doi>10.1016/S0304-3975(98)00308-9]
• 20: Marcin Jurdzinski , Ranko Lazic, Alternation-free modal mu-calculus for data trees, Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, p.131-140, July 10-14, 2007 [doi>10.1109/LICS.2007.11]
• 21: Michael Kaminski , Nissim Francez, Finite-memory automata, Theoretical Computer Science, v.134 n.2, p.329-363, Nov. 21, 1994 [doi>10.1016/0304-3975(94)90242-9]
• 22: Emanuel Kieronski, Small Substructures and Decidability Issues for First-Order Logic with Two Variables, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, p.448-457, June 26-29, 2005 [doi>10.1109/LICS.2005.49]
• 23: Martens, W., and Niehren, J. 2005. Minimizing tree automata for unranked trees. In Proceedings of the International Symposium on Database Programming Languages. Lecture Notes in Computer Science, vol. 3774. Springer-Verlag, New York, 232--246.
• 24: Marx, M. 2005. First order paths in ordered trees. In ICDT'05. Lecture Notes in Computer Science, vol. 3363. Springer-Verlag, Berlin, Germany, 114--128.
• 25: Mortimer, M. 1975. On languages with two variables. Zeitschr. f. math. Logik u. Grundlagen d. Math. 21, 135--140.
• 26: Frank Neven , Thomas Schwentick, XPath Containment in the Presence of Disjunction, DTDs, and Variables, Proceedings of the 9th International Conference on Database Theory, p.315-329, January 08-10, 2003
• 27: Frank Neven , Thomas Schwentick, Query automata over finite trees, Theoretical Computer Science, v.275 n.1-2, p.633-674, March 28 2002 [doi>10.1016/S0304-3975(01)00301-2]
• 28: Neeraj Verma, K., Seidl, H., and Schwentick, T. 2005. On the complexity of equational horn clauses. In CADE'05, Lecture Notes in Computer Science, vol. 3632. Springer-Verlag, Berlin, Germany, 337--352.
• 29: Frank Neven , Thomas Schwentick , Victor Vianu, Finite state machines for strings over infinite alphabets, ACM Transactions on Computational Logic (TOCL), v.5 n.3, p.403-435, July 2004 [doi>10.1145/1013560.1013562]
• 30: Christos H. Papadimitriou, On the complexity of integer programming, Journal of the ACM (JACM), v.28 n.4, p.765-768, Oct. 1981 [doi>10.1145/322276.322287]
• 31: XML Path Language (XPath), W3C Recommendation 16 November 1999. Available at http://www.w3.org/TR/xpath.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic

Additional Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages

  H. Information Systems
  H.2 DATABASE MANAGEMENT
      H.2.1 Logical Design
      H.2.3 Languages
          Subjects: Query languages

  I. Computing Methodologies
  I.7 DOCUMENT AND TEXT PROCESSING
      I.7.2 Document Preparation

General Terms:
Algorithms, Design, Languages, Theory

Keywords:
DTDs, Integrity constraints, XML, consistency, implications