{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:56:41Z","timestamp":1762459001098,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540156482"},{"type":"electronic","value":"9783540395270"}],"license":[{"start":{"date-parts":[[1985,1,1]],"date-time":"1985-01-01T00:00:00Z","timestamp":473385600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1985]]},"DOI":"10.1007\/3-540-15648-8_7","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T18:22:11Z","timestamp":1330194131000},"page":"79-88","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":61,"title":["Automata, tableaux, and temporal logics"],"prefix":"10.1007","author":[{"given":"E. Allen","family":"Emerson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"7_CR1","unstructured":"Abrahamson, K., Decidability and Expressiveness of Logics of Processes, PhD Thesis, Univ. of Washington, 1980."},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Ben-Ari, M., Manna, Z., and Pnueli, A., The Temporal Logic of Branching Time. 8th Annual ACM Symp. on Principles of Programming Languages, 1981.","DOI":"10.1145\/567532.567551"},{"key":"7_CR3","unstructured":"Clarke, E. M., and Emerson, E. A., Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic, Proceedings of the IBM Workshop on Logics of Programs, Springer-Verlag Lecture Notes in Computer Science #131, 1981."},{"key":"7_CR4","unstructured":"Clarke, E. M., Emerson, E. A., and Sistla, A. P., Automatic Verification of Finite State Concurrent Programs: A Practical Approach, POPL83."},{"key":"7_CR5","first-page":"169","volume":"85","author":"E. A. Emerson","year":"1980","unstructured":"Emerson, E. A., and Clarke, E. M., Characterizing Correctness Properties of Parallel Programs Using Fixpoints, Proc. ICALP 80, LNCS Vol. 85, Springer Verlag, 1980, pp. 169\u2013181.","journal-title":"LNCS"},{"key":"7_CR6","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E. A. Emerson","year":"1982","unstructured":"Emerson, E. A., and Clarke, E. M., Using Branching Time Logic to Synthesize Synchronization Skeletons, Science of Computer Programming, vol. 2, pp. 241\u2013266, 1982.","journal-title":"Science of Computer Programming"},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Emerson, E. A., and Halpern, J. Y., Decision Procedures and Expressiveness in the Temporal Logic of Branching Time. 14th Annual ACM Symp. on Theory of Computing, 1982.","DOI":"10.1145\/800070.802190"},{"key":"7_CR8","unstructured":"Emerson, E. A., and Halpern, J. Y., 'sometimes\u2019 and \u2018Not Never\u2019 Revisited: On Branching versus Linear Time. POPL83."},{"key":"7_CR9","unstructured":"Emerson, E. A., and Lei, C. L., Modalities for Model Checking: Branching Time Strikes Back, to be presented at the 12th Annual ACM Symposium on Principles of Programming Languages."},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Emerson, E. A., and Sistla, A. P., Deciding Branching Time Logic, 16 Annual ACM Symp. on Theory of Computing, 1984.","DOI":"10.1145\/800057.808661"},{"key":"7_CR11","doi-asserted-by":"crossref","unstructured":"Hossley, R., and Rackoff, C, The Emptiness Problem For Automata on Infinite Trees, Proc. 13th IEEE Symp. Switching and Automata Theory, pp. 121\u2013124, 1972.","DOI":"10.1109\/SWAT.1972.28"},{"key":"7_CR12","unstructured":"Koren, T. and Pnueli, A., There exist decidable context-free propositional dynamic logics, CMU Workshop on Logics of Programs, Springer LNCS #164, pp. 313\u2013325, 1983."},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"McNaughton, R., Testing and Generating Infinite Sequences by a Finite Automaton, Information and Control, vol. 9, 1966.","DOI":"10.1016\/S0019-9958(66)80013-X"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Manna, Z., and Pnueli, A., The modal logic of programs, Proc. 6th Int. Colloquium on Automata, Languages, and Programming, Springer-Verlag Lecture Notes in Computer Science #71, pp. 385\u2013410, 1979.","DOI":"10.1007\/3-540-09510-1_31"},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"Meyer, A. R., Weak Monadic Second Order Theory of Successor is Not Elementary Recursive, Boston Logic Colloquium, Springer-Verlag Lecture Notes in Mathematics #453, 1974.","DOI":"10.1007\/BFb0064872"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Pnueli, A., The Temporal Logic of Programs, 19th Annual Symp. on Foundations of Computer Science, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"7_CR17","first-page":"1","volume":"141","author":"M. Rabin","year":"1969","unstructured":"Rabin, M., Decidability of Second order Theories and Automata on Infinite Trees, Trans. Amer. Math. Society, vol. 141, pp. 1\u201335, 1969.","journal-title":"Trans. Amer. Math. Society"},{"key":"7_CR18","unstructured":"Rabin, M., Automata on Infinite Trees and the Synthesis Problem, Hebrew Univ., Tech. Report no. 37, 1970."},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Streett, R., Propositional Dynamic Logic of Looping and Converse (PhD Thesis), MIT Lab for Computer Science, TR-263, 1981. (a revised version appears in Information and Control, vol. 54, pp. 121\u2013141, 1982.)","DOI":"10.1016\/S0019-9958(82)91258-X"},{"key":"7_CR20","unstructured":"Wolper, P., A Translation from Full Branching Time Temporal Logic to One Letter Propositional Dynamic Logic with Looping, unpublished manuscript, 1982."},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Vardi, M., and Wolper, P., Yet Another Process Logic, CMU Workshop on Logics of Programs, Springer-Verlag, 1983.","DOI":"10.1007\/3-540-12896-4_383"},{"key":"7_CR22","doi-asserted-by":"crossref","unstructured":"Wolper, P., Vardi, M., and Sistla, A., Reasoning about Infinite Computations, 24th FOCS, 1983.","DOI":"10.1109\/SFCS.1983.51"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Vardi, M. and Wolper, P., Automata Theoretic Techniques for Modal Logics of Programs, pp. 446\u2013455, STOC84.","DOI":"10.1145\/800057.808711"},{"key":"7_CR24","unstructured":"Vardi, M. and Stockmeyer, L., Improved Upper and Lower Bounds for Modal Logics of Programs, to be presented at STOC85."}],"container-title":["Lecture Notes in Computer Science","Logics of Programs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-15648-8_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T20:22:34Z","timestamp":1742588554000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-15648-8_7"}},"subtitle":["Extended Abstract"],"short-title":[],"issued":{"date-parts":[[1985]]},"ISBN":["9783540156482","9783540395270"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-15648-8_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1985]]},"assertion":[{"value":"31 May 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}