{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:53:51Z","timestamp":1725663231071},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540156482"},{"type":"electronic","value":"9783540395270"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1985]]},"DOI":"10.1007\/3-540-15648-8_27","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T18:21:29Z","timestamp":1330194089000},"page":"359-372","source":"Crossref","is-referenced-by-count":3,"title":["Fixpoints and program looping: Reductions from the Propositional mu-calculus into Propositional Dynamic Logics of Looping"],"prefix":"10.1007","author":[{"given":"Robert S.","family":"Streett","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"27_CR1","unstructured":"de Bakker, J., and de Roever, W. P. (1973), A Calculus for Recursive Program Schemes, First International Colloquium on Automata, Languages, and Programming, 167\u2013196."},{"key":"27_CR2","volume-title":"Recursive Program Schemes: Semantics and Proof Theory","author":"W. P. Roever de","year":"1974","unstructured":"de Roever, W. P. (1974), Recursive Program Schemes: Semantics and Proof Theory, Ph.D. thesis, Free University, Amsterdam."},{"key":"27_CR3","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1016\/S0022-0000(76)80034-7","volume":"12","author":"A. Ehrenfeucht","year":"1976","unstructured":"Ehrenfeucht, A., and Zeiger, P. (1976), Complexity Measures for Regular Expressions, Journal of Computer System Science12, 134\u2013146.","journal-title":"Journal of Computer System Science"},{"key":"27_CR4","doi-asserted-by":"crossref","unstructured":"Emerson, A. E., and Clarke, E. C. (1980), Characterizing Correctness Properties of Parallel Programs using Fixpoints, Seventh International Colloquium on Automata, Languages and Programming, 169\u2013181.","DOI":"10.1007\/3-540-10003-2_69"},{"key":"27_CR5","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 Science18, 194\u2013211.","journal-title":"Journal of Computer System Science"},{"key":"27_CR6","doi-asserted-by":"crossref","unstructured":"Harel, D. (1979), First Order Dynamic Logic, Springer-Verlag Lecture Notes in Computer Science68.","DOI":"10.1007\/3-540-09237-4"},{"key":"27_CR7","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1016\/S0019-9958(82)90553-8","volume":"55","author":"D. Harel","year":"1984","unstructured":"Harel, D., and Sherman, R. (1984), Looping versus Repeating in Dynamic Logic, Information and Control55, 175\u2013192, 1984.","journal-title":"Information and Control"},{"key":"27_CR8","unstructured":"Hitchcock, P., and Park, D. M. R. (1973), Induction Rules and Termination Proofs, First International Colloquium on Automata, Languages, and Programming, 225\u2013251."},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"Hossley, R., and Rackoff, C. W. (1972), The Emptiness Problem for Automata on Infinite Trees, Thirteenth IEEE Symposium on Switching and Automata Theory, 121\u2013124.","DOI":"10.1109\/SWAT.1972.28"},{"key":"27_CR10","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 Control29, 243\u2013251.","journal-title":"Information and Control"},{"key":"27_CR11","doi-asserted-by":"crossref","unstructured":"Kozen, D. (1982), Results on the Propositional Mu-Calculus, Ninth International Colloquium on Automata, Languages, and Programming, 348\u2013359.","DOI":"10.1007\/BFb0012782"},{"key":"27_CR12","doi-asserted-by":"crossref","unstructured":"Kozen, D., and Parikh, R. J. (1983), A Decision Procedure for the Propositional MuCalculus, Second Workshop on Logics of Programs.","DOI":"10.1007\/3-540-12896-4_370"},{"key":"27_CR13","unstructured":"Kripke, S. A. (1963), Semantical Considerations on Modal Logics, Acta Philosophica Fennica."},{"key":"27_CR14","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1016\/S0019-9958(66)80013-X","volume":"9","author":"R. McNaughton","year":"1966","unstructured":"McNaughton, R. (1966), Testing and Generating Infinite Sequences by a Finite Automaton, Information and Control9, 521\u2013530.","journal-title":"Information and Control"},{"key":"27_CR15","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 Mathematics453.","DOI":"10.1007\/BFb0064872"},{"key":"27_CR16","unstructured":"Niwinski, D. (1984), The Propositional Mu-Calculus is More Expressive than the Propositional Dynamic Logic of Looping, unpublished manuscript."},{"key":"27_CR17","doi-asserted-by":"crossref","unstructured":"Parikh, R. J. (1979), A Decidability Result for a Second Order Process Logic, Nineteenth IEEE Symposium on the Foundations of Computer Science, 177\u2013183.","DOI":"10.1109\/SFCS.1978.2"},{"key":"27_CR18","unstructured":"Parikh, R. J. (1983a), Cake Cutting, Dynamic Logic, Games, and Fairness, Second Workshop on Logics of Programs."},{"key":"27_CR19","doi-asserted-by":"crossref","unstructured":"Parikh, R. J. (1983b), Propositional Game Logic, Twenty-third IEEE Symposium on the Foundations of Computer Science.","DOI":"10.1109\/SFCS.1983.47"},{"key":"27_CR20","unstructured":"Park, D. M. R. (1970), Fixpoint Induction and Proof of Program Semantics, Machine Intelligence5, Edinburgh University Press."},{"key":"27_CR21","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/0304-3975(76)90022-0","volume":"3","author":"D. M. R. Park","year":"1976","unstructured":"Park, D. M. R. (1976), Finiteness is Mu-Ineffable, Theoretical Computer Science3, 173\u2013181.","journal-title":"Theoretical Computer Science"},{"key":"27_CR22","unstructured":"Pnueli, A., and Sherman, R. (1983),Propositional Dynamic Logic of Looping Flowcharts, Technical Report, Weizmann Institute of Science."},{"key":"27_CR23","doi-asserted-by":"crossref","unstructured":"Pratt, V. R. (1976), Semantical Considerations on Floyd-Hoare Logic, Seventeenth IEEE Symposium on Foundations of Computer Science, 109\u2013121.","DOI":"10.1109\/SFCS.1976.27"},{"key":"27_CR24","doi-asserted-by":"crossref","unstructured":"Pratt, V. R. (1982), A Decidable Mu-Calculus: Preliminary Report, Twenty-second IEEE Symposium on the Foundations of Computer Science, 421\u2013427.","DOI":"10.1109\/SFCS.1981.4"},{"key":"27_CR25","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 Society141, 1\u201335.","journal-title":"Transactions of the American Mathematical Society"},{"key":"27_CR26","unstructured":"Sherman, R. (1984), Variants of Propositional Dynamic Logic, Ph.D. thesis, Weizmann Institute of Science."},{"key":"27_CR27","unstructured":"Streett, R. S. (1980), A Propositional Dynamic Logic for Reasoning About Program Divergence, M.S. thesis, Massachusetts Institute of Technology."},{"key":"27_CR28","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":"27_CR29","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 Elemantarily Decidable, Information and Control54, 121\u2013141.","journal-title":"Information and Control"},{"key":"27_CR30","first-page":"465","volume":"172","author":"R. S. Streett","year":"1984","unstructured":"Streett, R. S., and Emerson, E. A. (1984), The Propositional Mu-Calculus is Elementary, Eleventh International Colloquium on Automata, Languages, and Programming, Springer-Verlag Lecture Notes in Computer Science172, 465\u2013472.","journal-title":"Eleventh International Colloquium on Automata, Languages, and Programming, Springer-Verlag Lecture Notes in Computer Science"},{"key":"27_CR31","doi-asserted-by":"crossref","unstructured":"Streett, R. S., and Emerson, E. A. (1985), An Automata Theoretic Decision Procedure for the Propositional Mu-Calculus, in preparation.","DOI":"10.1007\/3-540-13345-3_43"},{"key":"27_CR32","doi-asserted-by":"crossref","unstructured":"Vardi, M. Y., and Stockmeyer, L. (1984), Improved Upper and Lower Bounds for Modal Logics of Programs, unpublished paper.","DOI":"10.1145\/22145.22173"},{"key":"27_CR33","doi-asserted-by":"crossref","unstructured":"Vardi, M., and Wolper, P (1984), Automata Theoretic Techniques for Modal Logics of Programs, Sixteenth ACM Symposium on the Theory of Computing.","DOI":"10.1145\/800057.808711"}],"container-title":["Lecture Notes in Computer Science","Logics of Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-15648-8_27.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T01:35:08Z","timestamp":1640914508000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-15648-8_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1985]]},"ISBN":["9783540156482","9783540395270"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-15648-8_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1985]]}}}