{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T11:05:50Z","timestamp":1768907150506,"version":"3.49.0"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2009,6,10]],"date-time":"2009-06-10T00:00:00Z","timestamp":1244592000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J of Log Lang and Inf"],"published-print":{"date-parts":[[2009,10]]},"DOI":"10.1007\/s10849-009-9093-x","type":"journal-article","created":{"date-parts":[[2009,6,9]],"date-time":"2009-06-09T08:54:32Z","timestamp":1244537672000},"page":"593-624","source":"Crossref","is-referenced-by-count":8,"title":["Branching-Time Logics Repeatedly Referring to States"],"prefix":"10.1007","volume":"18","author":[{"given":"Volker","family":"Weber","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,6,10]]},"reference":[{"issue":"3","key":"9093_CR1","doi-asserted-by":"crossref","first-page":"296","DOI":"10.1145\/772062.772064","volume":"4","author":"M. Adler","year":"2003","unstructured":"Adler M., Immerman N. (2003) An n! lower bound on formula size. ACM Transactions on Computational Logic 4(3): 296\u2013314","journal-title":"ACM Transactions on Computational Logic"},{"key":"9093_CR2","doi-asserted-by":"crossref","unstructured":"Areces, C., Blackburn, P., & Marx, M. (1999). A road-map on complexity for hybrid logics. In Proceedings of the 13th international workshop on computer science logic (CSL \u201999), LNCS (Vol. 1683, pp. 307\u2013321). Springer.","DOI":"10.1007\/3-540-48168-0_22"},{"issue":"3","key":"9093_CR3","doi-asserted-by":"crossref","first-page":"977","DOI":"10.2307\/2695090","volume":"66","author":"C. Areces","year":"2001","unstructured":"Areces C., Blackburn P., Marx M. (2001) Hybrid logics: Characterization, interpolation and complexity. Journal of Symbolic Logic 66(3): 977\u20131010","journal-title":"Journal of Symbolic Logic"},{"key":"9093_CR4","doi-asserted-by":"crossref","unstructured":"Areces, C., & ten Cate, B. (2007). Hybrid logics. In Handbook of modal logic, studies in logic (Vol. 3, pp. 821\u2013868). New York: Elsevier.","DOI":"10.1016\/S1570-2464(07)80017-6"},{"key":"9093_CR5","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/BF01257083","volume":"20","author":"M. Ben-Ari","year":"1983","unstructured":"Ben-Ari M., Pnueli A., Manna Z. (1983) The temporal logic of branching time. Acta Informatica 20: 207\u2013226","journal-title":"Acta Informatica"},{"key":"9093_CR6","doi-asserted-by":"crossref","unstructured":"Bozzelli, L. (2008). The complexity of CTL* + linear past. In Proceedings of the 11th international conference on foundations of software science and computational structures (FOSSACS 2008), LNCS (Vol. 4962, pp. 186\u2013200). Springer.","DOI":"10.1007\/978-3-540-78499-9_14"},{"issue":"3","key":"9093_CR7","doi-asserted-by":"crossref","first-page":"374","DOI":"10.1016\/0022-0000(86)90036-X","volume":"32","author":"B.S. Chlebus","year":"1986","unstructured":"Chlebus B.S. (1986) Domino-tiling games. Journal of Computer and System Sciences 32(3): 374\u2013392","journal-title":"Journal of Computer and System Sciences"},{"key":"9093_CR8","unstructured":"Clarke, E. M., & Emerson, E. A. (1981). Design and synthesis of synchronization skeletons using branching- time temporal logic. In Proceedings logic of programs, LNCS (Vol. 131, pp. 52\u201371). Springer."},{"key":"9093_CR9","volume-title":"Model checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke E.M., Grumberg O., Peled D.A. (1999) Model checking. MIT Press, Cambridge"},{"key":"9093_CR10","doi-asserted-by":"crossref","unstructured":"Demri, S., & Lazi\u0107, R. (2006). LTL with the freeze quantifier and register automata. In Proceedings of the 21th IEEE symposium on logic in computer science (LICS 2006) (pp. 17\u201326). IEEE.","DOI":"10.1109\/LICS.2006.31"},{"issue":"1","key":"9093_CR11","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"Emerson E.A., Halpern J.Y. (1986) \u201cSometimes\u201d and \u201cnot never\u201d revisited: On branching versus linear time temporal logic. Journal of the ACM 33(1): 151\u2013178","journal-title":"Journal of the ACM"},{"key":"9093_CR12","doi-asserted-by":"crossref","unstructured":"Emerson, E. A., & Jutla, C. S. (1991). Tree automata, mu-calculus and determinacy. In Proceedings of the 32nd IEEE annual symposium on foundations of computer science (FOCS \u201991) (pp. 368\u2013377). IEEE.","DOI":"10.1109\/SFCS.1991.185392"},{"issue":"3","key":"9093_CR13","doi-asserted-by":"crossref","first-page":"279","DOI":"10.1016\/j.jal.2005.06.010","volume":"4","author":"M. Franceschet","year":"2006","unstructured":"Franceschet M., de Rijke M. (2006) Model checking hybrid logics (with an application to semistructured data). Journal of Applied Logic 4(3): 279\u2013304","journal-title":"Journal of Applied Logic"},{"key":"9093_CR14","doi-asserted-by":"crossref","unstructured":"Franceschet, M., de Rijke, M., & Schlingloff, B. H. (2003). Hybrid logics on linear structures: Expressivity and complexity. In Proceedings of the 10th international symposium on temporal representation and reasoning\/4th international conference on temporal logic (TIME-ICTL 2003) (pp. 192\u2013202). IEEE.","DOI":"10.1109\/TIME.2003.1214893"},{"key":"9093_CR15","doi-asserted-by":"crossref","unstructured":"Goranko, V. (1994). Temporal logic with reference pointers. In Proceedings of the first international conference on temporal logic (ICTL \u201994), LNCS (Vol. 827, pp. 133\u2013148). Springer.","DOI":"10.1007\/BFb0013985"},{"key":"9093_CR16","doi-asserted-by":"crossref","unstructured":"Grumberg, O., & Veith, H. (Eds.). (2008). 25 Years of model checking\u2014history, achievements, perspectives, LNCS (Vol. 5000). Springer.","DOI":"10.1007\/978-3-540-69850-0"},{"key":"9093_CR17","doi-asserted-by":"crossref","unstructured":"Hafer, T., & Thomas, W. (1987). Computation tree logic CTL* and path quantifiers in the monadic theory of the binary tree. In Proceedings of the 14th international colloquium on automata, languages and programming (ICALP \u201987), LNCS (Vol. 267, pp. 269\u2013279). Springer.","DOI":"10.1007\/3-540-18088-5_22"},{"key":"9093_CR18","doi-asserted-by":"crossref","unstructured":"Jurdzi\u0144ski, M., & Lazi\u0107, R. (2007). Alternation-free mu-calculus for data trees. In Proceedings of the 22th IEEE symposium on logic in computer science (LICS 2007), IEEE.","DOI":"10.1109\/LICS.2007.11"},{"key":"9093_CR19","doi-asserted-by":"crossref","unstructured":"Kupferman, O., & Vardi, M. Y. (2006). Memoryful branching-time logic. In Proceedings of the 21st IEEE symposium on logic in computer science (LICS 2006) (pp. 265\u2013274). IEEE.","DOI":"10.1109\/LICS.2006.34"},{"key":"9093_CR20","doi-asserted-by":"crossref","unstructured":"Laroussinie, F., Markey, N., & Schnoebelen, P. (2002). Temporal logic with forgettable past. In Proceedings of the 17th IEEE symposium on logic in computer science (LICS 2002) (pp. 383\u2013392). IEEE.","DOI":"10.1109\/LICS.2002.1029846"},{"issue":"2","key":"9093_CR21","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1016\/0304-3975(95)00035-U","volume":"148","author":"F. Laroussinie","year":"1995","unstructured":"Laroussinie F., Schnoebelen P. (1995) A hierarchy of temporal logics with past. Theoretical Computer Science 148(2): 303\u2013324","journal-title":"Theoretical Computer Science"},{"issue":"1-2","key":"9093_CR22","first-page":"236","volume":"156","author":"F. Laroussinie","year":"2000","unstructured":"Laroussinie F., Schnoebelen P. (2000) Specification in CTL\u00a0+\u00a0Past for verification in CTL. Logic in Computer Science 156(1-2): 236\u2013263","journal-title":"Logic in Computer Science"},{"key":"9093_CR23","doi-asserted-by":"crossref","unstructured":"Moller, F., & Rabinovich, A. M. (1999). On the expressive power of CTL*. In Proceedings of the 14th annual IEEE symposium on logic in computer science (LICS \u201999) (pp. 360\u2013369). IEEE.","DOI":"10.1109\/LICS.1999.782631"},{"key":"9093_CR24","unstructured":"Mundhenk, M., Schneider, T., Schwentick, T., & Weber, V. (2005). Complexity of hybrid logics over transitive frames. In Proceedings of M4M-4, Humbold-Universit\u00e4t Berlin, Informatik-Berichte (Vol. 194, pp. 62\u201378)."},{"key":"9093_CR25","doi-asserted-by":"crossref","unstructured":"Rabin, M. (1970). Weakly definable relations and special automata. In Proceedings of symposium mathematical logic and foundations of set theory, North Holland (pp. 1\u201323).","DOI":"10.1016\/S0049-237X(08)71929-3"},{"key":"9093_CR26","doi-asserted-by":"crossref","unstructured":"Schwentick, T., & Weber, V. (2007). Bounded-variable fragments of hybrid logics. In Proceedings of the 24th annual symposium on theoretical aspects of computer science (STACS 2007), LNCS (Vol. 4393, pp. 561\u2013572). Springer.","DOI":"10.1007\/978-3-540-70918-3_48"},{"key":"9093_CR27","unstructured":"Stockmeyer, L. J. (1974). The complexity of decision problems in automata theory and logic. PhD thesis, MIT."},{"key":"9093_CR28","unstructured":"ten Cate, B., & Franceschet, M. (2005). On the complexity of hybrid logics with binders. In Proceedings of the 19th international workshop on computer science logic (CSL 2005), LNCS (Vol. 3634, pp. 339\u2013354). Springer."},{"key":"9093_CR29","first-page":"133","volume-title":"Handbook of theoretical computer science, Vol. B: Formal models and sematics","author":"W. Thomas","year":"1990","unstructured":"Thomas W. (1990) Automata on infinite objects. In: van Leeuwen J. (eds) Handbook of theoretical computer science, Vol. B: Formal models and sematics. Elsevier, MIT Press, pp 133\u2013192"},{"key":"9093_CR30","doi-asserted-by":"crossref","unstructured":"Vardi, M. Y. (1995). Alternating automata and program verification. In Computer science today, LNCS (Vol. 1000, pp. 471\u2013485). Heidelberg: Springer.","DOI":"10.1007\/BFb0015261"},{"key":"9093_CR31","doi-asserted-by":"crossref","unstructured":"Vardi, M. Y. (1998). Reasoning about the past with two-way automata. In Proceedings of the 25th international colloquium on automata, languages and programming (ICALP \u201998), LNCS (Vol. 1443, pp. 628\u2013641). Springer.","DOI":"10.1007\/BFb0055090"},{"key":"9093_CR32","doi-asserted-by":"crossref","unstructured":"Vardi, M. Y. (2007). Automata-theoretic techniques for temporal reasoning. In Handbook of modal logic, studies in logic (Vol. 3, pp. 971\u2013989). Elsevier.","DOI":"10.1016\/S1570-2464(07)80020-6"},{"key":"9093_CR33","unstructured":"Vardi, M. Y., & Stockmeyer, L. J. (1985). Improved upper and lower bounds for modal logics of programs: Preliminary report. In Proceedings of the 17th annual ACM symposium on theory of computing (STOC \u201985), ACM (pp. 240\u2013251)."},{"key":"9093_CR34","doi-asserted-by":"crossref","unstructured":"Wilke, T. (1999). CTL+ is exponentially more succinct than CTL. In Proceedings of the 19th conference on foundations of software technology and theoretical computer science (FSTTCS), LNCS (Vol. 1738, pp. 110\u2013121). Springer.","DOI":"10.1007\/3-540-46691-6_9"},{"key":"9093_CR35","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1016\/S0304-3975(98)00009-7","volume":"200","author":"W. Zielonka","year":"1998","unstructured":"Zielonka W. (1998) Infinite games on finitely coloured graphs with applications to automata and infinite trees. Theoretical Computer Science 200: 135\u2013183","journal-title":"Theoretical Computer Science"}],"container-title":["Journal of Logic, Language and Information"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10849-009-9093-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10849-009-9093-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10849-009-9093-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T02:31:02Z","timestamp":1559269862000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10849-009-9093-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,6,10]]},"references-count":35,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2009,10]]}},"alternative-id":["9093"],"URL":"https:\/\/doi.org\/10.1007\/s10849-009-9093-x","relation":{},"ISSN":["0925-8531","1572-9583"],"issn-type":[{"value":"0925-8531","type":"print"},{"value":"1572-9583","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,6,10]]}}}