{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T03:14:00Z","timestamp":1772075640804,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540616047","type":"print"},{"value":"9783540706250","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61604-7_60","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:03:28Z","timestamp":1330293808000},"page":"263-277","source":"Crossref","is-referenced-by-count":107,"title":["On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic"],"prefix":"10.1007","author":[{"given":"David","family":"Janin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Igor","family":"Walukiewicz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur, D. Peled, and W. Penczek. Model-checking of causality properties. In LICS '95, pages 90\u2013100, 1995.","DOI":"10.1109\/LICS.1995.523247"},{"key":"17_CR2","first-page":"177","volume":"66","author":"A. Amir","year":"1985","unstructured":"A. Amir. Separation in nonlinear time models. Information and Computation, 66:177\u2013203, 1985.","journal-title":"Information and Computation"},{"key":"17_CR3","unstructured":"A. Arnold. Finite Transition Systems. Masson, Prentice-Hall, 1994."},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"B. Banieqbal and H. Barringer. Temporal logic with fixed points. volume 398 of LNCS, pages 62\u201374. Springer-Verlag, 1989.","DOI":"10.1007\/3-540-51803-7_22"},{"key":"17_CR5","unstructured":"J. Benthem. Languages in Action: Categories, Lambdas and Dynamic Logic, volume 130 of Studies in Logic. North-Holland, 1991."},{"key":"17_CR6","unstructured":"J. Benthem and J. Bergstra. Logic of transition systems. Report P9308, Programming Research Group, University of Amsterdam, 1993."},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, R. Echahed, and P. Habermehl. On verification problem of nonregular properties of nonregular processes. In LICS '95, pages 123\u2013133, 1995.","DOI":"10.1109\/LICS.1995.523250"},{"key":"17_CR8","doi-asserted-by":"crossref","first-page":"210","DOI":"10.1016\/0022-0000(87)90025-0","volume":"34","author":"I. Castellani","year":"1987","unstructured":"I. Castellani. Bisimulations and abstraction homomorphisms. Journal of Computer and System Sciences, 34:210\u2013235, 1987.","journal-title":"Journal of Computer and System Sciences"},{"key":"17_CR9","first-page":"145","volume":"581","author":"M. Dam","year":"1992","unstructured":"M. Dam. CTL* and ECTL* as a fragments of the modal \u039c-calculus. In CAAP'92, volume 581 of LNCS, pages 145\u2013165, 1992.","journal-title":"LNCS"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"E. A. Emerson. Temporal and modal logic. In J. Leeuven, editor, Handbook of Theoretical Computer Science Vol.B, pages 995\u20131072. Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and C. Jutla. Tree automata, mu-calculus and determinacy. In Proc. FOCS 91, 1991.","DOI":"10.1109\/SFCS.1991.185392"},{"key":"17_CR12","first-page":"353","volume":"939","author":"J. Esparza","year":"1995","unstructured":"J. Esparza and A. Kiehn. On the model checking problem for branching time logics and basic parallel processes. In CAV '95, volume 939 of LNCS, pages 353\u2013366, 1995.","journal-title":"LNCS"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"A. Gabbay, A. Pnueli, S. Shelah, and J. Stavi. On the temporal analysis of fairness. In 7th Ann. ACM Symp. on Principles of Programming Languages, pages 163\u2013173, 1980.","DOI":"10.1145\/567446.567462"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"D. Gabbay. Expressive functional completeness in tense logic. In Aspects of Philosophical Logic, pages 91\u2013117. Reidel, 1981.","DOI":"10.1007\/978-94-009-8384-7_4"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"H. Gaifman. On local and non-local properties. In Herbrand Symposium, Logic Colloquium'81, pages 105\u2013135. North-Holland, 1982.","DOI":"10.1016\/S0049-237X(08)71879-2"},{"key":"17_CR16","first-page":"269","volume":"267","author":"T. Hafer","year":"1987","unstructured":"T. Hafer and W. Thomas. Computation tree logic CTL* and path quantifiers in the monadic theory of the binary tree. In 14th Internat. Coll. on Automata, Languages and Programming, volume 267 of LNCS, pages 269\u2013279, 1987.","journal-title":"LNCS"},{"key":"17_CR17","doi-asserted-by":"crossref","first-page":"857","DOI":"10.1137\/0222054","volume":"22","author":"D. Harel","year":"1993","unstructured":"D. Harel and D. Raz. Deciding properties of nonregular programs. SIAM J. Comput, 22:857\u2013874, 1993.","journal-title":"SIAM J. Comput"},{"key":"17_CR18","unstructured":"D. Janin. Propri\u00e9r\u00e9s logiques du non-d\u00e9terminisme et \u039c-calcul modal. PhD thesis, LaBRI \u2014 Universit\u00e9 de Bordeaux I, 1995. Available from http:\/\/www.labri.u-bordeaux.fr\/\u223cjanin."},{"key":"17_CR19","first-page":"552","volume":"969","author":"D. Janin","year":"1995","unstructured":"D. Janin and I. Walukiewicz. Automata for the \u039c-calculus and related results. In MFCS '95, volume 969 of LNCS, pages 552\u2013562, 1995.","journal-title":"LNCS"},{"key":"17_CR20","unstructured":"H. Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, University of California, 1968."},{"key":"17_CR21","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"D. Kozen. Results on the prepositional mu-calculus. Theoretical Computer Science, 27:333\u2013354, 1983.","journal-title":"Theoretical Computer Science"},{"key":"17_CR22","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1989","unstructured":"R. Milner. Communication and Concurrency. Prentice-Hall, Englewood Clifs, 1989."},{"key":"17_CR23","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0304-3975(87)90133-2","volume":"54","author":"D. Muller","year":"1987","unstructured":"D. Muller and P. Schupp. Alternating automata on infinite trees. Theoretical Computer Science, 54:267\u2013276, 1987.","journal-title":"Theoretical Computer Science"},{"key":"17_CR24","doi-asserted-by":"crossref","unstructured":"D. Niwi\u0144ski. Fixed points vs. infinite generation. In LICS '88, pages 402\u2013409, 1988.","DOI":"10.1109\/LICS.1988.5137"},{"key":"17_CR25","unstructured":"G. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus University, 1981."},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The temporal logic of programs. In 18th Symposium on Foundations of Computer Science, pages 46\u201357, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"17_CR27","first-page":"1","volume":"141","author":"M. Rabin","year":"1969","unstructured":"M. Rabin. Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc., 141:1\u201335, 1969.","journal-title":"Trans. Amer. Math. Soc."},{"key":"17_CR28","unstructured":"C. S. Stirling. Modal and temporal logics. In S.Abramsky, D.Gabbay, and T.Maibaum, editors, Handbook of Logic in Comuter Science, pages 477\u2013563. Oxford University Press, 1991."},{"key":"17_CR29","doi-asserted-by":"crossref","unstructured":"P. Thiagarajan. A trace based extension of linear time temporal logic. In LICS, pages 438\u2013447, 1994.","DOI":"10.1109\/LICS.1994.316047"},{"key":"17_CR30","first-page":"278","volume":"458","author":"R. Glabbeek van","year":"1990","unstructured":"R. van Glabbeek. The linear time \u2014 branching time spectrum. In CONCUR'90, volume 458 of LNCS, pages 278\u2013297, 1990.","journal-title":"LNCS"},{"key":"17_CR31","first-page":"401","volume":"1046","author":"I. Walukiewicz","year":"1996","unstructured":"I. Walukiewicz. Monadic second order logic on tree-like structures. In STACS '96, volume 1046 of LNCS, pages 401\u2013414, 1996.","journal-title":"LNCS"},{"key":"17_CR32","series-title":"Chapter Models for Concurrency","first-page":"1","volume-title":"Handbook of Logic in Computer Science, volume 4","author":"G. Winskel","year":"1995","unstructured":"G. Winskel and M. Nielsen. Handbook of Logic in Computer Science, volume 4, Chapter Models for Concurrency, pages 1\u2013148. Clarendon Press-Oxford, 1995."}],"container-title":["Lecture Notes in Computer Science","CONCUR '96: Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61604-7_60.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T23:22:41Z","timestamp":1742599361000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61604-7_60"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540616047","9783540706250"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/3-540-61604-7_60","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}