{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T03:25:37Z","timestamp":1778297137295,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540581796","type":"print"},{"value":"9783540484691","type":"electronic"}],"license":[{"start":{"date-parts":[[1994,1,1]],"date-time":"1994-01-01T00:00:00Z","timestamp":757382400000},"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":[[1994]]},"DOI":"10.1007\/3-540-58179-0_66","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T10:25:44Z","timestamp":1330251944000},"page":"338-350","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":38,"title":["An improved algorithm for the evaluation of fixpoint expressions"],"prefix":"10.1007","author":[{"given":"David E.","family":"Long","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anca","family":"Browne","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edmund M.","family":"Clarke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Somesh","family":"Jha","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wilfredo R.","family":"Marrero","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"28_CR1","doi-asserted-by":"crossref","unstructured":"H. R. Andersen. Model checking and boolean graphs. In B. Krieg-Bruckner, editor, Proceedings of the Fourth European Symposium on Programming, volume 582 of Lecture Notes in Computer Science. Springer-Verlag, February 1992.","DOI":"10.1007\/3-540-55253-7_1"},{"key":"28_CR2","doi-asserted-by":"crossref","unstructured":"G. V. Bochmann and D. K. Probst, editors. Proceedings of the Fourth Workshop on Computer-Aided Verification, volume 663 of Lecture Notes in Computer Science. Springer-Verlag, July 1992.","DOI":"10.1007\/3-540-56496-9"},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8), 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"28_CR4","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, June 1990."},{"key":"28_CR5","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, I. A. Draghicescu, and R. P. Kurshan. A unified approach for showing language containment and equivalence between various types of \u03a9-automata. In A. Arnold and N. D. Jones, editors, Proceedings of the 15th Colloquium on Trees in Algebra and Programming, volume 407 of Lecture Notes in Computer Science. Springer-Verlag, May 1990.","DOI":"10.1007\/3-540-52590-4_43"},{"key":"28_CR6","volume-title":"volume 131 of Lecture Notes in Computer Science","author":"E. M. Clarke","year":"1981","unstructured":"E. M. Clarke and E. A. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. In Logic of Programs: Workshop, Yorktown Heights, NY, May 1981, volume 131 of Lecture Notes in Computer Science. Springer-Verlag, 1981."},{"issue":"8","key":"28_CR7","doi-asserted-by":"publisher","first-page":"725","DOI":"10.1007\/BF00264284","volume":"27","author":"R. Cleaveland","year":"1990","unstructured":"R. Cleaveland. Tableau-based model checking in the propositional mu-calculus. Acta Informatica, 27(8):725\u2013747, 1990.","journal-title":"Acta Informatica"},{"key":"28_CR8","unstructured":"R. Cleaveland, M. Klein, and B. Steffen. Faster model checking for the modal mu-calculus. In Bochmann and Probst [2]."},{"issue":"2","key":"28_CR9","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/BF01383878","volume":"2","author":"R. Cleaveland","year":"1993","unstructured":"R. Cleaveland and B. Steffen. A linear-time model-checking algorithm for the alternation-free modal mu-calculus. Formal Methods in System Design, 2(2):121\u2013147, April 1993.","journal-title":"Formal Methods in System Design"},{"key":"28_CR10","volume-title":"volume 407 of Lecture Notes in Computer Science","author":"O. Coudert","year":"1989","unstructured":"O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines based on symbolic execution. In J. Sifakis, editor, Proceedings of the 1989 International Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, volume 407 of Lecture Notes in Computer Science. Springer-Verlag, June 1989."},{"key":"28_CR11","unstructured":"E. A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional mu-calculus. In Proceedings of the First Annual Symposium on Logic in Computer Science. IEEE Computer Society Press, June 1986."},{"key":"28_CR12","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M. J. Fischer","year":"1979","unstructured":"M. J. Fischer and R. E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18:194\u2013211, 1979.","journal-title":"Journal of Computer and System Sciences"},{"key":"28_CR13","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 mu-calculus. Theoretical Computer Science, 27:333\u2013354, December 1983.","journal-title":"Theoretical Computer Science"},{"key":"28_CR14","unstructured":"K. G. Larsen. Efficient local correctness checking. In Bochmann and Probst [2]."},{"key":"28_CR15","unstructured":"A. Mader. Tableau recycling. In Bochmann and Probst [2]."},{"key":"28_CR16","doi-asserted-by":"crossref","unstructured":"R. Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer-Verlag, 1980.","DOI":"10.1007\/3-540-10235-3"},{"issue":"1","key":"28_CR17","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/0304-3975(90)90110-4","volume":"89","author":"C. Stirling","year":"1991","unstructured":"C. Stirling and D. J. Walker. Local model checking in the modal mu-calculus. Theoretical Computer Science, 89(1):161\u2013177, October 1991.","journal-title":"Theoretical Computer Science"},{"key":"28_CR18","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","unstructured":"A. Tarski. A lattice-theoretic fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285\u2013309, 1955.","journal-title":"Pacific Journal of Mathematics"},{"key":"28_CR19","doi-asserted-by":"crossref","unstructured":"G. Winskel. Model checking in the modal \u039d-calculus. In Proceedings of the Sixteenth International Colloquium on Automata, Languages, and Programming, 1989.","DOI":"10.1007\/BFb0035797"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58179-0_66","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T01:19:04Z","timestamp":1640913544000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58179-0_66"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581796","9783540484691"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-58179-0_66","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994]]},"assertion":[{"value":"7 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}