{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:28:19Z","timestamp":1761611299834},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540631651"},{"type":"electronic","value":"9783540691945"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63165-8_198","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:11:21Z","timestamp":1330279881000},"page":"419-429","source":"Crossref","is-referenced-by-count":27,"title":["Model checking the full modal mu-calculus for infinite sequential processes"],"prefix":"10.1007","author":[{"given":"Olaf","family":"Burkart","sequence":"first","affiliation":[]},{"given":"Bernhard","family":"Steffen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"40_CR1","unstructured":"O. Burkart and J. Esparza. More Infinite Results. In INFINITY '96, volume 6 of ENTCS, 23 pages. Elsevier Science B.V., 1997."},{"key":"40_CR2","doi-asserted-by":"crossref","unstructured":"O. Burkart and Y.-M. Quemener. Model-Checking of Infinite Graphs Defined by Graph Grammars. In INFINITY '96, volume 6 of ENTCS, 15 pages. Elsevier Science B.V., 1997.","DOI":"10.1016\/S1571-0661(05)80677-2"},{"key":"40_CR3","doi-asserted-by":"crossref","unstructured":"J.C. Bradfield. The Modal mu-Calculus Alternation Hierarchy is Strict. In CONCUR '96, LNCS 1119, pages 233\u2013246. Springer, 1996.","DOI":"10.1007\/3-540-61604-7_58"},{"key":"40_CR4","doi-asserted-by":"crossref","unstructured":"O. Burkart and B. Steffen. Model Checking for Context-Free Processes. In CONCUR '92, LNCS 630, pages 123\u2013137. Springer, 1992.","DOI":"10.1007\/BFb0084787"},{"key":"40_CR5","first-page":"89","volume":"2","author":"O. Burkart","year":"1995","unstructured":"O. Burkart and B. Steffen. Composition, Decomposition and Model-Checking of Pushdown Processes. Nordic Journal of Computing, 2:89\u2013125, 1995.","journal-title":"Nordic Journal of Computing"},{"key":"40_CR6","doi-asserted-by":"crossref","unstructured":"O. Burkart and B. Steffen. Model Checking the Full-Modal Mu-Calculus for Infinite Sequential Processes. Technical Report LFCS-97-355, University of Edinburgh, April 1997.","DOI":"10.1007\/3-540-63165-8_198"},{"key":"40_CR7","doi-asserted-by":"crossref","unstructured":"D. Caucal. On Infinite Transition Graphs Having a Decidable Monadic Theory. In ICALP '96, LNCS 1099, pages 194\u2013205. Springer, 1996.","DOI":"10.1007\/3-540-61440-0_128"},{"key":"40_CR8","first-page":"410","volume":"663","author":"R. Cleaveland","year":"1992","unstructured":"R. Cleaveland, M. Klein, and B. Steffen. Faster Model Checking for the Modal Mu-Calculus. In CAV '92, LNCS 663, pages 410\u2013422, 1992.","journal-title":"CAV '92, LNCS"},{"key":"40_CR9","doi-asserted-by":"crossref","unstructured":"B. Courcelle. Graph Rewriting: An Algebraic and Logic Approach. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 5, pages 193\u2013242. Elsevier Science Publisher B.V., 1990.","DOI":"10.1016\/B978-0-444-88074-1.50010-X"},{"issue":"3","key":"40_CR10","first-page":"364","volume":"1","author":"H. Hungar","year":"1994","unstructured":"H. Hungar and B. Steffen. Local Model-Checking for Context-Free Processes. Nordic Journal of Computing, 1(3):364\u2013385, 1994.","journal-title":"Nordic Journal of Computing"},{"key":"40_CR11","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"D. Kozen. Results on the Propositional \u03bc-Calculus. Theoretical Computer Science, 27:333\u2013354, 1983.","journal-title":"Theoretical Computer Science"},{"key":"40_CR12","doi-asserted-by":"crossref","unstructured":"D.E. Long, A. Browne, E.M. Clarke, S. Jha, and W.R. Marrero. An Improved Algorithm for the Evaluation of Fixpoint Expressions. In CAV '94, LNCS 818, pages 338\u2013350. Springer, 1994.","DOI":"10.1007\/3-540-58179-0_66"},{"key":"40_CR13","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0304-3975(85)90087-8","volume":"37","author":"D.E. Muller","year":"1985","unstructured":"D.E. Muller and P.E. Schupp. The Theory of Ends, Pushdown Automata, and Second-Order Logic. Theoretical Computer Science, 37:51\u201375, 1985.","journal-title":"Theoretical Computer Science"},{"key":"40_CR14","first-page":"1","volume":"141","author":"R.O. Rabin","year":"1969","unstructured":"R.O. Rabin. Decidability of Second-Order Theories and Automata on Infinite Trees. Transactions of the AMS, 141:1\u201335, 1969.","journal-title":"Transactions of the AMS"},{"key":"40_CR15","doi-asserted-by":"crossref","unstructured":"I. Walukiewicz. Pushdown Processes: Games and Model-Checking. In CAV '96, LNCS 1102. Springer, 1996.","DOI":"10.1007\/3-540-61474-5_58"}],"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-63165-8_198.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:16:26Z","timestamp":1605629786000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63165-8_198"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631651","9783540691945"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-63165-8_198","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}