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
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Afanasiev, L., Franceschet, M., Marx, M., de Rijke, M.: CTL model checking for processing simple XPath queries. In: TIME 2004, pp. 117–124 (2004)
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)
Barceló, P., Libkin, L.: Temporal logics over unranked trees. In: LICS 2005, pp. 31–40 (2005)
Bhat, G., Cleaveland, R.: Efficient model checking via the equational μ-calculus. In: LICS 1996, pp. 304–312 (1996)
Bloem, R., Engelfriet, J.: Monadic second order logic and node relations on graphs and trees. Struct. in Logic and Comp. Science, 144–161 (1997)
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)
ten Cate, B.: Expressivity of XPath with transitive closure. In: PODS 2006, pp. 328–337 (2006)
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)
Clarke, E., Schlingloff, B.-H.: Model Checking. In: Handbook of Automated Reasoning, pp. 1635–1790. Elsevier, Amsterdam (2001)
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)
Compton, K., Henson, C.W.: A uniform method for proving lower bounds on the computational complexity of logical theories. APAL 48, 1–79 (1990)
Emerson, E.A., Lei, C.-L.: Modalities for model checking: branching time logic strikes back. Sci. Comput. Program 8, 275–306 (1987)
Filiot, E., Niehren, J., Talbot, J.-M., Tison, S.: Composing monadic queries in trees. In: PLAN-X 2006, pp. 61–70 (2006)
Frick, M., Grohe, M.: The complexity of first-order and monadic second-order logic revisited. In: LICS 2002, pp. 215–224 (2002)
Goris, E., Marx, M.: Looping caterpillars. In: LICS 2005, pp. 51–60 (2005)
Gottlob, G., Koch, C.: Monadic datalog and the expressive power of languages for web information extraction. J. ACM 51, 74–113 (2004)
Gottlob, G., Koch, C., Pichler, R., Segoufin, L.: The complexity of XPath query evaluation and XML typing. J. ACM 52, 284–335 (2005)
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)
Klarlund, N., Schwentick, T., Suciu, D.: XML: model, schemas, types, logics, and queries. In: Logics for Emerging Applications of Databases, Springer, Heidelberg (2003)
Koch, C.: Processing queries on tree-structured data efficiently. In: PODS 2006, pp. 213–224 (2006)
Kupferman, O., Pnueli, A.: Once and for all. In: LICS 1995, pp. 25–35 (1995)
Lakshmanan, L., Ramesh, G., Wang, H., Zhao, Z.: On testing satisfiability of tree pattern queries. In: VLDB 2004, pp. 120–131 (2004)
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)
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)
Marx, M.: Conditional XPath. ACM TODS 30(4) (2005)
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)
Miklau, G., Suciu, D.: Containment and equivalence for a fragment of XPath. J. ACM 51(1), 2–45 (2004)
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)
Neven, F., Schwentick, T.: Query automata over finite trees. TCS 275, 633–674 (2002)
Niwinski, D.: Fixed points vs. infinite generation. In: LICS 1988, pp. 402–409 (1988)
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)
Schlingloff, B.-H.: Expressive completeness of temporal logic of trees. Journal of Applied Non-Classical Logics 2, 157–180 (1992)
Schwentick, T.: On diving in trees. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol. 1893, pp. 660–669. Springer, Heidelberg (2000)
Sistla, A.P., Clarke, E.: The complexity of propositional linear temporal logics. J. ACM 32, 733–749 (1985)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)