{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:02:10Z","timestamp":1725483730366},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540679011"},{"type":"electronic","value":"9783540446125"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44612-5_58","type":"book-chapter","created":{"date-parts":[[2007,5,5]],"date-time":"2007-05-05T13:28:20Z","timestamp":1178371700000},"page":"629-639","source":"Crossref","is-referenced-by-count":1,"title":["Why so Many Temporal Logics Climb up the Trees?"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Rabinovich","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shahar","family":"Maoz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2001,6,1]]},"reference":[{"key":"58_CR1","series-title":"Lect Notes Comput Sci","first-page":"52","volume-title":"Design and verification of synchronous skeletons using branching time temporal logic","author":"E.M. Clarke","year":"1981","unstructured":"E.M. Clarke and E.A. Emerson (1981). Design and verification of synchronous skeletons using branching time temporal logic. LNCS 131:52\u201371."},{"key":"58_CR2","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, E.A. Emerson and A.P. Sistla. Automatic verification of finite state concurrent system using temporal logic. In: POPL, 1983.","DOI":"10.1145\/567067.567080"},{"key":"58_CR3","doi-asserted-by":"crossref","first-page":"129","DOI":"10.4064\/fm-49-2-129-141","volume":"49","author":"A. Ehrenfeucht","year":"1961","unstructured":"A. Ehrenfeucht. An application of games to the completeness problem for formalized theories. Fundamenta mathematicae 49, 129\u2013141, 1961.","journal-title":"Fundamenta mathematicae"},{"key":"58_CR4","volume-title":"Handbook of Theoretical Computer Science","author":"E.A. Emerson","year":"1990","unstructured":"E.A. Emerson (1990). Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B. Elsevier, Amsterdam, 1990."},{"key":"58_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/3-540-60915-6_3","volume-title":"Automated Temporal Reasoning about Reactive Systems","author":"E.A. Emerson","year":"1996","unstructured":"E.A. Emerson (1996). Automated Temporal Reasoning about Reactive Systems. LNCS vol. 1043, pp. 41\u2013101, Springer Verlag 1996."},{"key":"58_CR6","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and J.Y. Halpern (1982). Decision procedures and expressiveness in the temporal logic of branching time. In STOC\u201982. pp. 169\u2013180.","DOI":"10.1145\/800070.802190"},{"issue":"1","key":"58_CR7","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"E.A. Emerson and J.Y. Halpern (1986). \u2019sometimes\u2019 and \u2018not never\u2019 revisited: on branching versus linear time temporal logics. Journal of the ACM 33(1):151\u2013178.","journal-title":"Journal of the ACM"},{"key":"58_CR8","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and C.L. Lei. Modalities for model checking: branching time strikes back. 12th ACM Symp. on POPL, pp. 84\u201396, 1985.","DOI":"10.1145\/318593.318620"},{"key":"58_CR9","doi-asserted-by":"crossref","unstructured":"D. Gabbay, I. Hodkinson and M. Reynolds (1994). Temporal Logic. Oxford University Press.","DOI":"10.1007\/BFb0013976"},{"key":"58_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/3-540-18088-5_22","volume-title":"ICALP\u201987","author":"T. Hafer","year":"1987","unstructured":"T. Hafer and W. Thomas (1987). Computation tree logic CTL* and path quantifiers in the monadic theory of the binary tree. In ICALP\u201987, LNCS 267:269\u2013279. Springer-Verlag."},{"key":"58_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/3-540-48168-0_13","volume-title":"Quantitative Temporal Logic","author":"Y. Hirshfeld","year":"1999","unstructured":"Y. Hirshfeld and A. Rabinovich (1999). Quantitative Temporal Logic. LNCS 1683:172\u2013187, Springer-Verlag."},{"key":"58_CR12","series-title":"Lect Notes Comput Sci","first-page":"263","volume-title":"CONCUR\u201996","author":"D. Janin","year":"639","unstructured":"D. Janin and I. Walukiewicz (1996). On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. In CONCUR\u201996, LNCS 1119:263\u2013277, Springer-Verlag. 639"},{"key":"58_CR13","volume-title":"PhD Thesis","author":"H.W. Kamp","year":"1968","unstructured":"H.W. Kamp (1968). Tense logic and the theory of linear order. PhD Thesis, University of California, Los Angeles."},{"key":"58_CR14","doi-asserted-by":"crossref","unstructured":"L. Lamport (1980). \u201cSometimes\u201d is sometimes \u201dnot never\u201d-On the temporal logic of programs. In POPL\u201980. pp. 174\u2013185.","DOI":"10.1145\/567446.567463"},{"key":"58_CR15","unstructured":"S. Maoz (2000). Infinite Hierarchy of Temporal Logics over Branching Time Models. M.Sc. Thesis, Tel-Aviv University."},{"key":"58_CR16","unstructured":"R. Milner (1989). Communication and Concurrency. Prentice-Hall."},{"key":"58_CR17","doi-asserted-by":"crossref","unstructured":"F. Moller and A. Rabinovich (1999). On the expressive power of CTL*. Proceedings of fourteenth IEEE Symposium on Logic in Computer Science, 360\u2013369.","DOI":"10.1109\/LICS.1999.782631"},{"key":"58_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/BFb0017309","volume-title":"Theoretical Computer Science","author":"D.M.R. Park","year":"1981","unstructured":"D.M.R. Park (1981). Concurrency and automata on infinite sequences. LNCS 104:168\u2013183."}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Computer Science 2000"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44612-5_58","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T18:41:15Z","timestamp":1556390475000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44612-5_58"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540679011","9783540446125"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-44612-5_58","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}