{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T11:06:24Z","timestamp":1768907184162,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642040269","type":"print"},{"value":"9783642040276","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-04027-6_38","type":"book-chapter","created":{"date-parts":[[2009,9,14]],"date-time":"2009-09-14T17:27:52Z","timestamp":1252949272000},"page":"530-545","source":"Crossref","is-referenced-by-count":2,"title":["On the Complexity of Branching-Time Logics"],"prefix":"10.1007","author":[{"given":"Volker","family":"Weber","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"38_CR1","volume-title":"Principles of Model Checking","author":"C. Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"38_CR2","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/BF01257083","volume":"20","author":"M. Ben-Ari","year":"1983","unstructured":"Ben-Ari, M., Pnueli, A., Manna, Z.: The temporal logic of branching time. Acta Informatica\u00a020, 207\u2013226 (1983)","journal-title":"Acta Informatica"},{"key":"38_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/978-3-540-78499-9_14","volume-title":"Foundations of Software Science and Computational Structures","author":"L. Bozzelli","year":"2008","unstructured":"Bozzelli, L.: The complexity of CTL* + linear past. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol.\u00a04962, pp. 186\u2013200. Springer, Heidelberg (2008)"},{"issue":"3","key":"38_CR4","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1016\/0022-0000(86)90036-X","volume":"32","author":"B.S. Chlebus","year":"1986","unstructured":"Chlebus, B.S.: Domino-tiling games. J. Comput. Syst. Sci.\u00a032(3), 374\u2013392 (1986)","journal-title":"J. Comput. Syst. Sci."},{"key":"38_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"38_CR6","doi-asserted-by":"crossref","unstructured":"Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B, pp. 995\u20131072. Elsevier, MIT Press (1990)","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"38_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-10003-2_69","volume-title":"Automata, Languages and Programming","author":"E.A. Emerson","year":"1980","unstructured":"Emerson, E.A., Clarke, E.M.: Characterizing correctness properties of parallel programs using fixpoints. In: de Bakker, J.W., van Leeuwen, J. (eds.) ICALP 1980. LNCS, vol.\u00a085, pp. 169\u2013181. Springer, Heidelberg (1980)"},{"issue":"1","key":"38_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","volume":"30","author":"E.A. Emerson","year":"1985","unstructured":"Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. J. Comput. Syst. Sci.\u00a030(1), 1\u201324 (1985)","journal-title":"J. Comput. Syst. Sci."},{"issue":"1","key":"38_CR9","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: \u201cSometimes\u201d and \u201cnot never\u201d revisited: on branching versus linear time temporal logic. J. ACM\u00a033(1), 151\u2013178 (1986)","journal-title":"J. ACM"},{"key":"38_CR10","first-page":"368","volume-title":"Proc. of the 32nd FOCS 1991","author":"E.A. Emerson","year":"1991","unstructured":"Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus and determinacy. In: Proc. of the 32nd FOCS 1991, pp. 368\u2013377. IEEE, Los Alamitos (1991)"},{"issue":"1","key":"38_CR11","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1137\/S0097539793304741","volume":"29","author":"E.A. Emerson","year":"1999","unstructured":"Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs. SIAM J. Comput.\u00a029(1), 132\u2013158 (1999)","journal-title":"SIAM J. Comput."},{"key":"38_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/3-540-51803-7_36","volume-title":"Temporal Logic in Specification","author":"D.M. Gabbay","year":"1989","unstructured":"Gabbay, D.M.: The declarative past and imperative future: Executable temporal logic for interactive systems. In: Banieqbal, B., Pnueli, A., Barringer, H. (eds.) Temporal Logic in Specification. LNCS, vol.\u00a0398, pp. 409\u2013448. Springer, Heidelberg (1989)"},{"key":"38_CR13","series-title":"Lecture Notes in Computer Science","volume-title":"25 Years of Model Checking","year":"2008","unstructured":"Grumberg, O., Veith, H. (eds.): 25 Years of Model Checking. LNCS, vol.\u00a05000. Springer, Heidelberg (2008)"},{"key":"38_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"38_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"767","DOI":"10.1007\/3-540-45061-0_60","volume-title":"Automata, Languages and Programming","author":"J. Johannsen","year":"2003","unstructured":"Johannsen, J., Lange, M.: CTL\u2009+\u2009 is complete for double exponential time. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol.\u00a02719, pp. 767\u2013775. Springer, Heidelberg (2003)"},{"key":"38_CR16","first-page":"25","volume-title":"Proc. of the 10th LICS 1995","author":"O. Kupferman","year":"1995","unstructured":"Kupferman, O., Pnueli, A.: Once and for all. In: Proc. of the 10th LICS 1995, pp. 25\u201335. IEEE, Los Alamitos (1995)"},{"key":"38_CR17","first-page":"265","volume-title":"Proc. of the 21st LICS 2006","author":"O. Kupferman","year":"2006","unstructured":"Kupferman, O., Vardi, M.Y.: Memoryful branching-time logic. In: Proc. of the 21st LICS 2006, pp. 265\u2013274. IEEE, Los Alamitos (2006)"},{"issue":"2","key":"38_CR18","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O. Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM\u00a047(2), 312\u2013360 (2000)","journal-title":"J. ACM"},{"key":"38_CR19","first-page":"174","volume-title":"Proc. of the7th POPL 1980","author":"L. Lamport","year":"1980","unstructured":"Lamport, L.: \u201cSometimes\u201d is sometimes \u201cnot never\u201d. In: Proc. of the7th POPL 1980, pp. 174\u2013185. ACM Press, New York (1980)"},{"issue":"2","key":"38_CR20","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1016\/0304-3975(95)00035-U","volume":"148","author":"F. Laroussinie","year":"1995","unstructured":"Laroussinie, F., Schnoebelen, P.: A hierarchy of temporal logics with past. Theor. Comput. Sci.\u00a0148(2), 303\u2013324 (1995)","journal-title":"Theor. Comput. Sci."},{"issue":"1-2","key":"38_CR21","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1006\/inco.1999.2817","volume":"156","author":"F. Laroussinie","year":"2000","unstructured":"Laroussinie, F., Schnoebelen, P.: Specification in CTL+Past for verification in CTL. Inf. Comput.\u00a0156(1-2), 236\u2013263 (2000)","journal-title":"Inf. Comput."},{"key":"38_CR22","first-page":"1","volume":"141","author":"M.O. Rabin","year":"1969","unstructured":"Rabin, M.O.: Decidability of second order theories and automata on infinite trees. Trans. AMS\u00a0141, 1\u201335 (1969)","journal-title":"Trans. AMS"},{"key":"38_CR23","first-page":"251","volume-title":"Proc. of the 27th PODS 2008","author":"B. Cate ten","year":"2008","unstructured":"ten Cate, B., Segoufin, L.: XPath, transitive closure logic, and nested tree walking automata. In: Proc. of the 27th PODS 2008, pp. 251\u2013260. ACM Press, New York (2008)"},{"key":"38_CR24","doi-asserted-by":"crossref","unstructured":"Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B, pp. 133\u2013192. Elsevier, MIT Press (1990)","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"38_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1007\/BFb0015261","volume-title":"Computer Science Today","author":"M.Y. Vardi","year":"1995","unstructured":"Vardi, M.Y.: Alternating automata and program verification. In: van Leeuwen, J. (ed.) Computer Science Today. LNCS, vol.\u00a01000, pp. 471\u2013485. Springer, Heidelberg (1995)"},{"key":"38_CR26","first-page":"240","volume-title":"Proc. of the 17th STOC 1985","author":"M.Y. Vardi","year":"1985","unstructured":"Vardi, M.Y., Stockmeyer, L.J.: Improved upper and lower bounds for modal logics of programs. In: Proc. of the 17th STOC 1985, pp. 240\u2013251. ACM Press, New York (1985)"},{"key":"38_CR27","unstructured":"Weber, V.: On the complexity of branching-time logics. Available from arXiv:0906.2521 [cs.LO]"},{"key":"#cr-split#-38_CR28.1","doi-asserted-by":"crossref","unstructured":"Weber, V.: Branching-time logics repeatedly referring to states. Accepted to JoLLI (2009);","DOI":"10.1007\/s10849-009-9093-x"},{"key":"#cr-split#-38_CR28.2","unstructured":"An extended abstract appered in the procedings of HyLo (2007)"},{"key":"38_CR29","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/S0304-3975(98)00009-7","volume":"200","author":"W. Zielonka","year":"1998","unstructured":"Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata and infinite trees. Theoretical Computer Science\u00a0200, 135\u2013183 (1998)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04027-6_38","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T15:19:25Z","timestamp":1558538365000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04027-6_38"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642040269","9783642040276"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04027-6_38","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}