Skip to main content

Logics for Unordered Trees with Data Constraints on Siblings

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8977))

Abstract

We study counting monadic second-order logics (CMso) for unordered data trees. Our objective is to enhance this logic with data constraints for comparing string data values attached to sibling edges of a data tree. We show that CMso satisfiability becomes undecidable when adding data constraints between siblings that can check the equality of factors of data values. For more restricted data constraints that can only check the equality of prefixes, we show that it becomes decidable, and propose a related automaton model with good complexities. This restricted logic is relevant to applications such as checking well-formedness properties of semi-structured databases and file trees. Our decidability results are obtained by compilation of CMso to automata for unordered trees, where both are enhanced with data constraints in a novel manner.

This is a preview of subscription content, log in via an institution.

Buying options

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abiteboul, S., Bourhis, P., Muscholl, A., Wu, Z.: Recursive queries on trees and data trees. In: ICDT, pp. 93–104. ACM (2013)

    Google Scholar 

  2. Benzaken, V., Castagna, G., Nguyen, K., Siméon, J.: Static and dynamic semantics of NoSQL languages. In: POPL, pp. 101–114. ACM (2013)

    Google Scholar 

  3. Boiret, A., Hugot, V., Niehren, J., Treinen, R.: Deterministic Automata for Unordered Trees. In: Fifth International Symposium on Games, Automata, Logics and Formal Verification (Gandalf) (2014)

    Google Scholar 

  4. Bojanczyk, M., David, C., Muscholl, A., Schwentick, T., Segoufin, L.: Two-variable logic on data words. ACM Trans. Comput. Log. 12(4), 27 (2011)

    Article  MathSciNet  Google Scholar 

  5. Boneva, I., Talbot, J.-M.: Automata and Logics for Unranked and Unordered Trees. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 500–515. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  6. Büchi, J.R.: Weak second-order arithmetic and finite automata. Mathematical Logic Quarterly 6(1–6), 66–92 (1960)

    Article  MATH  Google Scholar 

  7. Comon, H., Dauchet, M., Gilleron, R., Löding, C., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree automata techniques and applications (2007). http://www.grappa.univ-lille3.fr/tata

  8. Courcelle, B.: The monadic second-order logic of graphs. i. recognizable sets of finite graphs. Information and computation 85(1), 12–75 (1990)

    Article  MATH  MathSciNet  Google Scholar 

  9. Figueira, D.: On XPath with transitive axes and data tests. In: ACM Symposium on Principles of Database, System, pp. 249–260 (2013)

    Google Scholar 

  10. Läuchli, H., Savioz, C.: Monadic second order definable relations on the binary tree. Journal of Symbol Logic 52(1), 219–226 (1987)

    Article  MATH  Google Scholar 

  11. Müller, M., Niehren, J., Treinen, R.: The first-order theory of ordering constraints over feature trees. In: 13th annual IEEE Symposium on Logic in Computer Sience, pp. 432–443 (1998)

    Google Scholar 

  12. Niehren, J., Podelski, A.: Feature automata and recognizable sets of feature trees. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) CAAP 1993, FASE 1993, and TAPSOFT 1993. LNCS, vol. 668, pp. 356–375. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  13. Rabin, M.: Automata on Infinite Objects and Church’s Problem. Number 13 in Conference Board of the Mathematical Sciences Regional Conference Series in Mathematics. AMS (1972)

    Google Scholar 

  14. Seidl, H., Schwentick, T., Muscholl, A.: Numerical document queries. In: ACM Symposium on Principles of Database Systems, pp. 155–166 (2003)

    Google Scholar 

  15. Seidl, H., Schwentick, T., Muscholl, A.: Counting in trees. In: Logic and Automata. Texts in Logic and Games, vol. 2, pp. 575–612. Amsterdam University Press (2008)

    Google Scholar 

  16. Smolka, G.: Feature constraint logics for unification grammars. Journal of Logic Programming 12, 51–87 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  17. Smolka, G., Treinen, R.: Records for logic programming. J. Log. Program. 18(3), 229–258 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  18. Stockmeyer, L., Meyer, A.: Word problems requiring exponential time. In: Symposium on the Theory of Computing. Association for Computing Machinery, Association for Computing Machinery, pp. 1–9 (1973)

    Google Scholar 

  19. Thatcher, J.W., Wright, J.B.: Generalized finite automata theory with an application to a decision problem of second-order logic. Mathematical systems theory 2(1), 57–81 (1968)

    Article  MathSciNet  Google Scholar 

  20. Thatcher, J.W., Wright, J.B.: Generalized finite automata with an application to the decision problem of second-order logic. Mathematical System Theory 2, 57–82 (1968)

    Article  MathSciNet  Google Scholar 

  21. Zilio, S.D., Lugiez, D.: XML Schema, Tree Logic and Sheaves Automata. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 246–263. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Vincent Hugot .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Boiret, A., Hugot, V., Niehren, J., Treinen, R. (2015). Logics for Unordered Trees with Data Constraints on Siblings. In: Dediu, AH., Formenti, E., Martín-Vide, C., Truthe, B. (eds) Language and Automata Theory and Applications. LATA 2015. Lecture Notes in Computer Science(), vol 8977. Springer, Cham. https://doi.org/10.1007/978-3-319-15579-1_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-15579-1_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-15578-4

  • Online ISBN: 978-3-319-15579-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics