{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:31:45Z","timestamp":1759638705222},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540784975"},{"type":"electronic","value":"9783540784999"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78499-9_14","type":"book-chapter","created":{"date-parts":[[2008,4,1]],"date-time":"2008-04-01T19:02:25Z","timestamp":1207076545000},"page":"186-200","source":"Crossref","is-referenced-by-count":5,"title":["The Complexity of CTL* + Linear Past"],"prefix":"10.1007","author":[{"given":"Laura","family":"Bozzelli","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","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)"},{"issue":"1","key":"14_CR2","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.: Sometimes and not never revisited: On branching versus linear time. Journal of the ACM\u00a033(1), 151\u2013178 (1986)","journal-title":"Journal of the ACM"},{"key":"14_CR3","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":"14_CR4","first-page":"25","volume-title":"Proc. 10th LICS","author":"O. Kupferman","year":"1995","unstructured":"Kupferman, O., Pnueli, A.: Once and For All. In: Proc. 10th LICS, pp. 25\u201335. IEEE Comp. Soc. Press, Los Alamitos (1995)"},{"key":"14_CR5","first-page":"224","volume-title":"Proc. 30th STOC","author":"O. Kupferman","year":"1998","unstructured":"Kupferman, O., Vardi, M.Y.: Weak alternating automata and tree automata emptiness. In: Proc. 30th STOC, pp. 224\u2013233. ACM, New York (1998)"},{"issue":"1","key":"14_CR6","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1145\/345099.345104","volume":"22","author":"O. Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y.: An automata-theoretic approach to modular model checking. ACM Trans. Program. Lang. Syst.\u00a022(1), 87\u2013128 (2000)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"14_CR7","first-page":"265","volume-title":"Proc. 21th LICS","author":"O. Kupferman","year":"2006","unstructured":"Kupferman, O., Vardi, M.Y.: Memoryful branching-time logic. In: Proc. 21th LICS, pp. 265\u2013274. IEEE Comp. Soc. Press, Los Alamitos (2006)"},{"issue":"2","key":"14_CR8","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"},{"issue":"2","key":"14_CR9","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. Theoretical Computer Science\u00a0148(2), 303\u2013324 (1995)","journal-title":"Theoretical Computer Science"},{"issue":"1\u20132","key":"14_CR10","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. Information and Computation\u00a0156(1\u20132), 236\u2013263 (2000)","journal-title":"Information and Computation"},{"key":"14_CR11","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(87)90133-2","volume":"54","author":"D.E. Muller","year":"1987","unstructured":"Muller, D.E., Schupp, P.E.: Alternating Automata on Infinite Trees. Theoretical Computer Science\u00a054, 267\u2013276 (1987)","journal-title":"Theoretical Computer Science"},{"doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, pp. 46\u201357 (1977)","key":"14_CR12","DOI":"10.1109\/SFCS.1977.32"},{"key":"14_CR13","first-page":"234","volume-title":"Proc. 18th LICS","author":"M. Pistore","year":"2003","unstructured":"Pistore, M., Vardi, M.Y.: The planning spectrum - one, two, three, infinity. In: Proc. 18th LICS, pp. 234\u2013243. IEEE Comp. Soc. Press, Los Alamitos (2003)"},{"key":"14_CR14","first-page":"250","volume-title":"Proc. 15th Annual POPL","author":"M.Y. Vardi","year":"1988","unstructured":"Vardi, M.Y.: A temporal fixpoint calculus. In: Proc. 15th Annual POPL, pp. 250\u2013259. ACM, New York (1988)"},{"key":"14_CR15","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)"},{"doi-asserted-by":"crossref","unstructured":"Vardi, M.Y., Stockmeyer, L.: Improved upper and lower bounds for modal logics of programs. In: Proc. 17th STOC, pp. 240\u2013251 (1985)","key":"14_CR16","DOI":"10.1145\/22145.22173"},{"issue":"1","key":"14_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation\u00a0115(1), 1\u201337 (1994)","journal-title":"Information and Computation"},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/3-540-46691-6_9","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"T. Wilke","year":"1999","unstructured":"Wilke, T.: CTL\u2009+\u2009 is exponentially more succinct than CTL. In: Pandu Rangan, C., Raman, V., Ramanujam, R. (eds.) FST TCS 1999. LNCS, vol.\u00a01738, pp. 110\u2013121. Springer, Heidelberg (1999)"},{"issue":"1\u20132","key":"14_CR19","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 on infinite trees. Theor. Comput. Sci.\u00a0200(1\u20132), 135\u2013183 (1998)","journal-title":"Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computational Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78499-9_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:11:28Z","timestamp":1619507488000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78499-9_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540784975","9783540784999"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78499-9_14","relation":{},"subject":[]}}