{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T15:52:55Z","timestamp":1742399575507},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540133452"},{"type":"electronic","value":"9783540388869"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1984]]},"DOI":"10.1007\/3-540-13345-3_43","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T18:04:17Z","timestamp":1330193057000},"page":"465-472","source":"Crossref","is-referenced-by-count":25,"title":["The propositional mu-calculus is elementary"],"prefix":"10.1007","author":[{"given":"Robert S.","family":"Streett","sequence":"first","affiliation":[]},{"given":"E. Allen","family":"Emerson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,28]]},"reference":[{"key":"43_CR1","unstructured":"deBakker, J., and deRoever, W. P. (1973), A Calculus for Recursive Program Schemes, in \"First International Colloquium on Automata, Languages, and Programming\", 167\u2013196."},{"key":"43_CR2","volume-title":"Recursive Program Schemes: Semantics and Proof Theory","author":"W. P. deRoever","year":"1974","unstructured":"deRoever, W. P. (1974), \"Recursive Program Schemes: Semantics and Proof Theory\", Ph. D. thesis, Free University, Amsterdam."},{"key":"43_CR3","doi-asserted-by":"crossref","unstructured":"Emerson, E. A., and Clarke, E. C. (1980), Characterizing Correctness Properties of Parallel Programs Using Fixpoints, in \"Seventh International Colloquium on Automata, Languages, and Programming\", 169\u2013181.","DOI":"10.1007\/3-540-10003-2_69"},{"key":"43_CR4","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M. J. Fischer","year":"1979","unstructured":"Fischer, M. J., and Ladner, R. E. (1979), Propositional Dynamic Logic of Regular Programs, Journal of Computer System Science 18, 194\u2013211.","journal-title":"Journal of Computer System Science"},{"key":"43_CR5","unstructured":"Hitchcock, P., and Park, D. M. R. (1973), Induction Rules and Termination Proofs, in \"First International Colloquium on Automata, Languages, and Programming\", 225\u2013251."},{"key":"43_CR6","doi-asserted-by":"crossref","unstructured":"Hossley, R., and Rackoff, C. W. (1972), The Emptiness Problem for Automata on Infinite Trees, in \"Thirteenth IEEE Symposium on Switching and Automata Theory\", 121\u2013124.","DOI":"10.1109\/SWAT.1972.28"},{"key":"43_CR7","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1016\/S0019-9958(75)90415-5","volume":"29","author":"A. J. Kfoury","year":"1975","unstructured":"Kfoury, A. J., and Park, D. M. R. (1975), On Termination of Program Schemes, Information and Control 29, 243\u2013251.","journal-title":"Information and Control"},{"key":"43_CR8","doi-asserted-by":"crossref","unstructured":"Kozen, D. (1982), Results on the Propositional Mu-Calculus, in \"Ninth International Colloquium on Automata, Languages, and Programming\", 348\u2013359.","DOI":"10.1007\/BFb0012782"},{"key":"43_CR9","doi-asserted-by":"crossref","unstructured":"Kozen, D., and Parikh, R. J. (1983), A Decision Procedure for the Propositional Mu-Calculus, to appear in \"Second Workshop on Logics of Programs\".","DOI":"10.1007\/3-540-12896-4_370"},{"key":"43_CR10","doi-asserted-by":"crossref","unstructured":"Meyer, A. R. (1974), Weak Monadic Second Order Theory of Successor is not Elementary Recursive, Boston Logic Colloquium, Springer-Verlag Lecture Notes in Mathematics 453.","DOI":"10.1007\/BFb0064872"},{"key":"43_CR11","doi-asserted-by":"crossref","unstructured":"Parikh, R. J. (1979), A Decidability Result for a Second Order Process Logic, in \"Nineteenth IEEE Symposium on the Foundations of Computing\", 177\u2013183.","DOI":"10.1109\/SFCS.1978.2"},{"key":"43_CR12","unstructured":"Parikh, R. J. (1983a), Cake Cutting, Dynamic Logic, Games, and Fairness, to appear in \"Second Workshop on Logics of Programs\"."},{"key":"43_CR13","doi-asserted-by":"crossref","unstructured":"Parikh, R. J. (1983b), Propositional Game Logic, to appear in \"Twenty-third IEEE Symposium on the Foundations of Computer Science\".","DOI":"10.1109\/SFCS.1983.47"},{"key":"43_CR14","unstructured":"Park, D. M. R. (1970), Fixpoint Induction and Proof of Program Semantics, Machine Intelligence 5, Edinburgh University Press."},{"key":"43_CR15","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/0304-3975(76)90022-0","volume":"3","author":"D. M. R. R. Park","year":"1976","unstructured":"Park, D. M. R. (1976), Finiteness is Mu-Ineffable, Theoretical Computer Science 3, 173\u2013181.","journal-title":"Theoretical Computer Science"},{"key":"43_CR16","doi-asserted-by":"crossref","unstructured":"Pratt, V. R. (1982), A Decidable Mu-Calculus: Preliminary Report, in \"Twenty-second IEEE Symposium on the Foundations of Computer Science\", 421\u2013427.","DOI":"10.1109\/SFCS.1981.4"},{"key":"43_CR17","first-page":"1","volume":"141","author":"M. O. Rabin","year":"1969","unstructured":"Rabin, M. O. (1969), Decidability of Second Order Theories and Automata on Infinite Trees\", Transactions of the American Mathematical Society 141, 1\u201335.","journal-title":"Transactions of the American Mathematical Society"},{"key":"43_CR18","doi-asserted-by":"crossref","unstructured":"Streett, R. S. (1981), \"Propositional Dynamic Logic of Looping and Converse\", MIT LCS Technical Report TR-263.","DOI":"10.1145\/800076.802492"},{"key":"43_CR19","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/S0019-9958(82)91258-X","volume":"54","author":"R. S. Streett","year":"1982","unstructured":"Streett, R. S. (1982), Propositional Dynamic Logic of Looping and Converse is Elementarily Decidable, Information and Control 54, 121\u2013141.","journal-title":"Information and Control"},{"key":"43_CR20","doi-asserted-by":"crossref","unstructured":"Vardi, M., and Wolper, P. (1984), Automata Theoretic Techniques for Modal Logics of Programs, to appear in \"Sixteenth ACM Symposium on the Theory of Computing\".","DOI":"10.1145\/800057.808711"}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-13345-3_43.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T17:40:25Z","timestamp":1687282825000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-13345-3_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1984]]},"ISBN":["9783540133452","9783540388869"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-13345-3_43","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1984]]}}}