Skip to main content
SpringerLink
Log in

Combining Temporal Logics for Querying XML Documents

  • Conference paper
Database Theory – ICDT 2007 (ICDT 2007)

Part of the book series: Lecture Notes in Computer Science ((LNISA,volume 4353))

Included in the following conference series:

Abstract

Close relationships between XML navigation and temporal logics have been discovered recently, in particular between logics LTL and CTL* and XPath navigation, and between the μ-calculus and navigation based on regular expressions. This opened up the possibility of bringing model-checking techniques into the field of XML, as documents are naturally represented as labeled transition systems. Most known results of this kind, however, are limited to Boolean or unary queries, which are not always sufficient for complex querying tasks.

Here we present a technique for combining temporal logics to capture n-ary XML queries expressible in two yardstick languages: FO and MSO. We show that by adding simple terms to the language, and combining a temporal logic for words together with a temporal logic for unary tree queries, one obtains logics that select arbitrary tuples of elements, and can thus be used as building blocks in complex query languages. We present general results on the expressiveness of such temporal logics, study their model-checking properties, and relate them to some common XML querying tasks.

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

Access this chapter

Log in via an institution
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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Afanasiev, L., Franceschet, M., Marx, M., de Rijke, M.: CTL model checking for processing simple XPath queries. In: TIME 2004, pp. 117–124 (2004)

    Google Scholar 

  2. Afanasiev, L., Blackburn, P., Dimitriou, I., Gaiffe, B., Goris, E., Marx, M., de Rijke, M.: PDL for ordered trees. J. Appl. Non-Classical Logics 15, 115–135 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  3. Barceló, P., Libkin, L.: Temporal logics over unranked trees. In: LICS 2005, pp. 31–40 (2005)

    Google Scholar 

  4. Bhat, G., Cleaveland, R.: Efficient model checking via the equational μ-calculus. In: LICS 1996, pp. 304–312 (1996)

    Google Scholar 

  5. Bloem, R., Engelfriet, J.: Monadic second order logic and node relations on graphs and trees. Struct. in Logic and Comp. Science, 144–161 (1997)

    Google Scholar 

  6. Cardelli, L., Ghelli, G.: A query language based on the ambient logic. In: Sands, D. (ed.) ESOP 2001 and ETAPS 2001. LNCS, vol. 2028, pp. 1–22. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  7. ten Cate, B.: Expressivity of XPath with transitive closure. In: PODS 2006, pp. 328–337 (2006)

    Google Scholar 

  8. Chen, Z., Jagadish, H.V., Lakshmanan, L., Paparizos, S.: From tree patterns to generalized tree patterns: on efficient evaluation of XQuery. In: Aberer, K., Koubarakis, M., Kalogeraki, V. (eds.) VLDB 2003. LNCS, vol. 2944, pp. 237–248. Springer, Heidelberg (2004)

    Google Scholar 

  9. Clarke, E., Schlingloff, B.-H.: Model Checking. In: Handbook of Automated Reasoning, pp. 1635–1790. Elsevier, Amsterdam (2001)

    Chapter  Google Scholar 

  10. Cleaveland, R., Steffen, B.: A linear-time model-checking algorithm for the alternation-free modal mu-calculus. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 48–58. Springer, Heidelberg (1992)

    Google Scholar 

  11. Compton, K., Henson, C.W.: A uniform method for proving lower bounds on the computational complexity of logical theories. APAL 48, 1–79 (1990)

    MATH  MathSciNet  Google Scholar 

  12. Emerson, E.A., Lei, C.-L.: Modalities for model checking: branching time logic strikes back. Sci. Comput. Program 8, 275–306 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  13. Filiot, E., Niehren, J., Talbot, J.-M., Tison, S.: Composing monadic queries in trees. In: PLAN-X 2006, pp. 61–70 (2006)

    Google Scholar 

  14. Frick, M., Grohe, M.: The complexity of first-order and monadic second-order logic revisited. In: LICS 2002, pp. 215–224 (2002)

    Google Scholar 

  15. Goris, E., Marx, M.: Looping caterpillars. In: LICS 2005, pp. 51–60 (2005)

    Google Scholar 

  16. Gottlob, G., Koch, C.: Monadic datalog and the expressive power of languages for web information extraction. J. ACM 51, 74–113 (2004)

    Article  MathSciNet  Google Scholar 

  17. Gottlob, G., Koch, C., Pichler, R., Segoufin, L.: The complexity of XPath query evaluation and XML typing. J. ACM 52, 284–335 (2005)

    Article  MathSciNet  Google Scholar 

  18. Hafer, T., Thomas, W.: Computation tree logic CTL* and path quantifiers in the monadic theory of the binary tree. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol. 267, pp. 269–279. Springer, Heidelberg (1987)

    Google Scholar 

  19. Klarlund, N., Schwentick, T., Suciu, D.: XML: model, schemas, types, logics, and queries. In: Logics for Emerging Applications of Databases, Springer, Heidelberg (2003)

    Google Scholar 

  20. Koch, C.: Processing queries on tree-structured data efficiently. In: PODS 2006, pp. 213–224 (2006)

    Google Scholar 

  21. Kupferman, O., Pnueli, A.: Once and for all. In: LICS 1995, pp. 25–35 (1995)

    Google Scholar 

  22. Lakshmanan, L., Ramesh, G., Wang, H., Zhao, Z.: On testing satisfiability of tree pattern queries. In: VLDB 2004, pp. 120–131 (2004)

    Google Scholar 

  23. Laroussinie, F., Markey, N., Schnoebelen, P.: Model checking CTL +  and FCTL is hard. In: Honsell, F., Miculan, M. (eds.) ETAPS 2001 and FOSSACS 2001. LNCS, vol. 2030, pp. 318–331. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  24. Libkin, L.: Logics for unranked trees: an overview. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 35–50. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  25. Marx, M.: Conditional XPath. ACM TODS 30(4) (2005)

    Google Scholar 

  26. Mateescu, R.: Local model-checking of modal mu-calculus on acyclic labeled transition systems. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol. 2280, pp. 281–295. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  27. Miklau, G., Suciu, D.: Containment and equivalence for a fragment of XPath. J. ACM 51(1), 2–45 (2004)

    Article  MathSciNet  Google Scholar 

  28. Neven, F.: Automata, logic, and XML. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol. 2471, pp. 2–26. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  29. Neven, F., Schwentick, T.: Query automata over finite trees. TCS 275, 633–674 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  30. Niwinski, D.: Fixed points vs. infinite generation. In: LICS 1988, pp. 402–409 (1988)

    Google Scholar 

  31. Planque, L., Niehren, J., Talbot, J.M., Tison, S.: N-ary queries by tree automata. In: Bierman, G., Koch, C. (eds.) DBPL 2005. LNCS, vol. 3774, pp. 217–231. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  32. Schlingloff, B.-H.: Expressive completeness of temporal logic of trees. Journal of Applied Non-Classical Logics 2, 157–180 (1992)

    MATH  MathSciNet  Google Scholar 

  33. Schwentick, T.: On diving in trees. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol. 1893, pp. 660–669. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  34. Sistla, A.P., Clarke, E.: The complexity of propositional linear temporal logics. J. ACM 32, 733–749 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  35. Vardi, M.Y.: Reasoning about the past with two-way automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 628–641. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  36. Vardi, M.Y.: Model checking for database theoreticians. In: Eiter, T., Libkin, L. (eds.) ICDT 2005. LNCS, vol. 3363, pp. 1–16. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Pontificia Universidad Católica de Chile,  

    Marcelo Arenas

  2. Universidad de Chile,  

    Pablo Barceló

  3. University of Edinburgh,  

    Leonid Libkin

Authors
  1. Marcelo Arenas
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pablo Barceló
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Leonid Libkin
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Technical University of Dortmund,  

    Thomas Schwentick

  2. Department of Computer Science and Engineering, University of Washington,  

    Dan Suciu

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Arenas, M., Barceló, P., Libkin, L. (2006). Combining Temporal Logics for Querying XML Documents. In: Schwentick, T., Suciu, D. (eds) Database Theory – ICDT 2007. ICDT 2007. Lecture Notes in Computer Science, vol 4353. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11965893_25

Download citation

  • DOI: https://doi.org/10.1007/11965893_25

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-69269-0

  • Online ISBN: 978-3-540-69270-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation