{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T08:10:07Z","timestamp":1736669407721,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540692690"},{"type":"electronic","value":"9783540692706"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11965893_25","type":"book-chapter","created":{"date-parts":[[2006,12,7]],"date-time":"2006-12-07T07:52:22Z","timestamp":1165477942000},"page":"359-373","source":"Crossref","is-referenced-by-count":7,"title":["Combining Temporal Logics for Querying XML Documents"],"prefix":"10.1007","author":[{"given":"Marcelo","family":"Arenas","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pablo","family":"Barcel\u00f3","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leonid","family":"Libkin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"Afanasiev, L., Franceschet, M., Marx, M., de Rijke, M.: CTL model checking for processing simple XPath queries. In: TIME 2004, pp. 117\u2013124 (2004)","key":"25_CR1","DOI":"10.1109\/TIME.2004.1314428"},{"key":"25_CR2","doi-asserted-by":"publisher","first-page":"115","DOI":"10.3166\/jancl.15.115-135","volume":"15","author":"L. Afanasiev","year":"2005","unstructured":"Afanasiev, L., Blackburn, P., Dimitriou, I., Gaiffe, B., Goris, E., Marx, M., de Rijke, M.: PDL for ordered trees. J. Appl. Non-Classical Logics\u00a015, 115\u2013135 (2005)","journal-title":"J. Appl. Non-Classical Logics"},{"doi-asserted-by":"crossref","unstructured":"Barcel\u00f3, P., Libkin, L.: Temporal logics over unranked trees. In: LICS 2005, pp. 31\u201340 (2005)","key":"25_CR3","DOI":"10.1007\/11523468_4"},{"doi-asserted-by":"crossref","unstructured":"Bhat, G., Cleaveland, R.: Efficient model checking via the equational \u03bc-calculus. In: LICS 1996, pp. 304\u2013312 (1996)","key":"25_CR4","DOI":"10.1109\/LICS.1996.561358"},{"doi-asserted-by":"crossref","unstructured":"Bloem, R., Engelfriet, J.: Monadic second order logic and node relations on graphs and trees. Struct. in Logic and Comp. Science, 144\u2013161 (1997)","key":"25_CR5","DOI":"10.1007\/3-540-63246-8_9"},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45309-1_1","volume-title":"Programming Languages and Systems","author":"L. Cardelli","year":"2001","unstructured":"Cardelli, L., Ghelli, G.: A query language based on the ambient logic. In: Sands, D. (ed.) ESOP 2001 and ETAPS 2001. LNCS, vol.\u00a02028, pp. 1\u201322. Springer, Heidelberg (2001)"},{"doi-asserted-by":"crossref","unstructured":"ten Cate, B.: Expressivity of XPath with transitive closure. In: PODS 2006, pp. 328\u2013337 (2006)","key":"25_CR7","DOI":"10.1145\/1142351.1142398"},{"key":"25_CR8","series-title":"Lecture Notes in Computer Science","first-page":"237","volume-title":"Databases, Information Systems, and Peer-to-Peer Computing","author":"Z. Chen","year":"2004","unstructured":"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.\u00a02944, pp. 237\u2013248. Springer, Heidelberg (2004)"},{"key":"25_CR9","doi-asserted-by":"publisher","first-page":"1635","DOI":"10.1016\/B978-044450813-3\/50026-6","volume-title":"Handbook of Automated Reasoning","author":"E. Clarke","year":"2001","unstructured":"Clarke, E., Schlingloff, B.-H.: Model Checking. In: Handbook of Automated Reasoning, pp. 1635\u20131790. Elsevier, Amsterdam (2001)"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1007\/3-540-55179-4_6","volume-title":"Computer Aided Verification","author":"R. Cleaveland","year":"1992","unstructured":"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.\u00a0575, pp. 48\u201358. Springer, Heidelberg (1992)"},{"key":"25_CR11","first-page":"1","volume":"48","author":"K. Compton","year":"1990","unstructured":"Compton, K., Henson, C.W.: A uniform method for proving lower bounds on the computational complexity of logical theories. APAL\u00a048, 1\u201379 (1990)","journal-title":"APAL"},{"key":"25_CR12","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E.A. Emerson","year":"1987","unstructured":"Emerson, E.A., Lei, C.-L.: Modalities for model checking: branching time logic strikes back. Sci. Comput. Program\u00a08, 275\u2013306 (1987)","journal-title":"Sci. Comput. Program"},{"unstructured":"Filiot, E., Niehren, J., Talbot, J.-M., Tison, S.: Composing monadic queries in trees. In: PLAN-X 2006, pp. 61\u201370 (2006)","key":"25_CR13"},{"doi-asserted-by":"crossref","unstructured":"Frick, M., Grohe, M.: The complexity of first-order and monadic second-order logic revisited. In: LICS 2002, pp. 215\u2013224 (2002)","key":"25_CR14","DOI":"10.1109\/LICS.2002.1029830"},{"doi-asserted-by":"crossref","unstructured":"Goris, E., Marx, M.: Looping caterpillars. In: LICS 2005, pp. 51\u201360 (2005)","key":"25_CR15","DOI":"10.1109\/LICS.2005.24"},{"key":"25_CR16","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1145\/962446.962450","volume":"51","author":"G. Gottlob","year":"2004","unstructured":"Gottlob, G., Koch, C.: Monadic datalog and the expressive power of languages for web information extraction. J. ACM\u00a051, 74\u2013113 (2004)","journal-title":"J. ACM"},{"key":"25_CR17","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1145\/1059513.1059520","volume":"52","author":"G. Gottlob","year":"2005","unstructured":"Gottlob, G., Koch, C., Pichler, R., Segoufin, L.: The complexity of XPath query evaluation and XML typing. J. ACM\u00a052, 284\u2013335 (2005)","journal-title":"J. ACM"},{"key":"25_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/3-540-18088-5_22","volume-title":"Automata, Languages and Programming","author":"T. Hafer","year":"1987","unstructured":"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.\u00a0267, pp. 269\u2013279. Springer, Heidelberg (1987)"},{"key":"25_CR19","volume-title":"Logics for Emerging Applications of Databases","author":"N. Klarlund","year":"2003","unstructured":"Klarlund, N., Schwentick, T., Suciu, D.: XML: model, schemas, types, logics, and queries. In: Logics for Emerging Applications of Databases, Springer, Heidelberg (2003)"},{"doi-asserted-by":"crossref","unstructured":"Koch, C.: Processing queries on tree-structured data efficiently. In: PODS 2006, pp. 213\u2013224 (2006)","key":"25_CR20","DOI":"10.1145\/1142351.1142382"},{"unstructured":"Kupferman, O., Pnueli, A.: Once and for all. In: LICS 1995, pp. 25\u201335 (1995)","key":"25_CR21"},{"doi-asserted-by":"crossref","unstructured":"Lakshmanan, L., Ramesh, G., Wang, H., Zhao, Z.: On testing satisfiability of tree pattern queries. In: VLDB 2004, pp. 120\u2013131 (2004)","key":"25_CR22","DOI":"10.1016\/B978-012088469-8.50014-0"},{"key":"25_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/3-540-45315-6_21","volume-title":"Foundations of Software Science and Computation Structures","author":"F. Laroussinie","year":"2001","unstructured":"Laroussinie, F., Markey, N., Schnoebelen, P.: Model checking CTL\u2009+\u2009 and FCTL is hard. In: Honsell, F., Miculan, M. (eds.) ETAPS 2001 and FOSSACS 2001. LNCS, vol.\u00a02030, pp. 318\u2013331. Springer, Heidelberg (2001)"},{"key":"25_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/11523468_4","volume-title":"Automata, Languages and Programming","author":"L. Libkin","year":"2005","unstructured":"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.\u00a03580, pp. 35\u201350. Springer, Heidelberg (2005)"},{"doi-asserted-by":"crossref","unstructured":"Marx, M.: Conditional XPath. ACM TODS\u00a030(4) (2005)","key":"25_CR25","DOI":"10.1145\/1114244.1114247"},{"key":"25_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/3-540-46002-0_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Mateescu","year":"2002","unstructured":"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.\u00a02280, pp. 281\u2013295. Springer, Heidelberg (2002)"},{"issue":"1","key":"25_CR27","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/962446.962448","volume":"51","author":"G. Miklau","year":"2004","unstructured":"Miklau, G., Suciu, D.: Containment and equivalence for a fragment of XPath. J. ACM\u00a051(1), 2\u201345 (2004)","journal-title":"J. ACM"},{"key":"25_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-45793-3_2","volume-title":"Computer Science Logic","author":"F. Neven","year":"2002","unstructured":"Neven, F.: Automata, logic, and XML. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol.\u00a02471, pp. 2\u201326. Springer, Heidelberg (2002)"},{"key":"25_CR29","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1016\/S0304-3975(01)00301-2","volume":"275","author":"F. Neven","year":"2002","unstructured":"Neven, F., Schwentick, T.: Query automata over finite trees. TCS\u00a0275, 633\u2013674 (2002)","journal-title":"TCS"},{"doi-asserted-by":"crossref","unstructured":"Niwinski, D.: Fixed points vs. infinite generation. In: LICS 1988, pp. 402\u2013409 (1988)","key":"25_CR30","DOI":"10.1109\/LICS.1988.5137"},{"key":"25_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/11601524_14","volume-title":"Database Programming Languages","author":"L. Planque","year":"2005","unstructured":"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.\u00a03774, pp. 217\u2013231. Springer, Heidelberg (2005)"},{"key":"25_CR32","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1080\/11663081.1992.10510780","volume":"2","author":"B.-H. Schlingloff","year":"1992","unstructured":"Schlingloff, B.-H.: Expressive completeness of temporal logic of trees. Journal of Applied Non-Classical Logics\u00a02, 157\u2013180 (1992)","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"25_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"660","DOI":"10.1007\/3-540-44612-5_61","volume-title":"Mathematical Foundations of Computer Science 2000","author":"T. Schwentick","year":"2000","unstructured":"Schwentick, T.: On diving in trees. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol.\u00a01893, pp. 660\u2013669. Springer, Heidelberg (2000)"},{"key":"25_CR34","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A.P. Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.: The complexity of propositional linear temporal logics. J. ACM\u00a032, 733\u2013749 (1985)","journal-title":"J. ACM"},{"key":"25_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"628","DOI":"10.1007\/BFb0055090","volume-title":"Automata, Languages and Programming","author":"M.Y. Vardi","year":"1998","unstructured":"Vardi, M.Y.: Reasoning about the past with two-way automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, pp. 628\u2013641. Springer, Heidelberg (1998)"},{"key":"25_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-30570-5_1","volume-title":"Database Theory - ICDT 2005","author":"M.Y. Vardi","year":"2004","unstructured":"Vardi, M.Y.: Model checking for database theoreticians. In: Eiter, T., Libkin, L. (eds.) ICDT 2005. LNCS, vol.\u00a03363, pp. 1\u201316. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Database Theory \u2013 ICDT 2007"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11965893_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T07:33:48Z","timestamp":1736667228000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11965893_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540692690","9783540692706"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/11965893_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}