{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,1]],"date-time":"2026-10-01T21:48:59Z","timestamp":1790891339941,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540610427","type":"print"},{"value":"9783540498742","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61042-1_41","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:11:59Z","timestamp":1330290719000},"page":"107-126","source":"Crossref","is-referenced-by-count":15,"title":["Efficient local model-checking for fragments of the modal \u039c-calculus"],"prefix":"10.1007","author":[{"given":"Girish","family":"Bhat","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rance","family":"Cleaveland","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"8_CR1","first-page":"1","volume-title":"Proceedings of the European Symposium on Programming, volume 582 of Lecture Notes in Computer Science","author":"H.R. Andersen","year":"1992","unstructured":"H.R. Andersen. Model checking and boolean graphs. In Proceedings of the European Symposium on Programming, volume 582 of Lecture Notes in Computer Science, pages 1\u201319, Rennes, France, March 1992. Springer-Verlag."},{"key":"8_CR2","first-page":"142","volume-title":"Computer Aided Verification (CAV '94), volume 818 of Lecture Notes in Computer Science","author":"O. Bernholtz","year":"1994","unstructured":"O. Bernholtz, M.Y. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking. In Dill [9], pages 142\u2013155."},{"key":"8_CR3","first-page":"388","volume-title":"Efficient on-the-fly model checking for CTL*","author":"G. Bhat","year":"1995","unstructured":"G. Bhat, R. Cleaveland, and O. Grumberg. Efficient on-the-fly model checking for CTL*. In Tenth Annual Symposium on Logic in Computer Science (LICS '95), pages 388\u2013397, San Diego, July 1995. IEEE Computer Society Press."},{"issue":"2","key":"8_CR4","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244\u2013263, April 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"8","key":"8_CR5","doi-asserted-by":"crossref","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, September 1990.","journal-title":"Acta Informatica"},{"key":"8_CR6","first-page":"410","volume-title":"Computer Aided Verification (CAV '92), volume 663 of Lecture Notes in Computer Science","author":"R. Cleaveland","year":"1992","unstructured":"R. Cleaveland, M. Klein, and B. Steffen. Faster model checking for the modal mu-calculus. In G.v. Bochmann and D.K. Probst, editors, Computer Aided Verification (CAV '92), volume 663 of Lecture Notes in Computer Science, pages 410\u2013422, Montr\u00e9al, June\/July 1992. Springer-Verlag."},{"issue":"1","key":"8_CR7","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1145\/151646.151648","volume":"15","author":"R. Cleaveland","year":"1993","unstructured":"R. Cleaveland, J. Parrow, and B. Steffen. The Concurrency Work-bench: A semantics-based tool for the verification of finite-state systems. ACM Transactions on Programming Languages and Systems, 15(1):36\u201372, January 1993.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"8_CR8","doi-asserted-by":"crossref","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:121\u2013147, 1993.","journal-title":"Formal Methods in System Design"},{"key":"8_CR9","volume-title":"Computer Aided Verification (CAV '94), volume 818 of Lecture Notes in Computer Science","year":"1994","unstructured":"D.L. Dill, editor. Computer Aided Verification (CAV '94), volume 818 of Lecture Notes in Computer Science, Stanford, California, June 1994. Springer-Verlag."},{"issue":"1","key":"8_CR10","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E.A. Emerson","year":"1986","unstructured":"E.A. Emerson and J.Y. Halpern. 'sometime\u2019 and \u2018not never\u2019 revisited: On branching versus linear time temporal logic. Journal of the Association for Computing Machinery, 33(1):151\u2013178, 1986.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"8_CR11","first-page":"385","volume-title":"Computer Aided Verification (CAV '93), volume 697 of Lecture Notes in Computer Science","author":"E.A. Emerson","year":"1993","unstructured":"E.A. Emerson, C. Jutla, and A.P. Sistla. On model-checking for fragments of \u039c-calculus. In C. Courcoubetis, editor, Computer Aided Verification (CAV '93), volume 697 of Lecture Notes in Computer Science, pages 385\u2013396, Elounda, Greece, June\/July 1993. Springer-Verlag."},{"key":"8_CR12","first-page":"267","volume-title":"Symposium on Logic in Computer Science (LICS '86)","author":"E.A. Emerson","year":"1986","unstructured":"E.A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional mu-calculus. In Symposium on Logic in Computer Science (LICS '86), pages 267\u2013278, Cambridge, Massachusetts, June 1986. IEEE Computer Society Press."},{"key":"8_CR13","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 propositional \u039c-calculus. Theoretical Computer Science, 27:333\u2013354, 1983.","journal-title":"Theoretical Computer Science"},{"key":"8_CR14","first-page":"338","volume-title":"Computer Aided Verification (CAV '94), volume 818 of Lecture Notes in Computer Science","author":"D.E. Long","year":"1994","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 Dill [9], pages 338\u2013350."},{"key":"8_CR15","first-page":"352","volume-title":"Computer Aided Verification (CAV '94), volume 818 of Lecture Notes in Computer Science","author":"O. Sokolsky","year":"1994","unstructured":"O. Sokolsky and S. Smolka. Incremental model-checking in the modal mu-calculus. In Dill [9], pages 352\u2013363."},{"key":"8_CR16","first-page":"369","volume-title":"TAPSOFT, volume 352 of Lecture Notes in Computer Science","author":"C. Stirling","year":"1989","unstructured":"C. Stirling and D. Walker. Local model checking in the modal mu-calculus. In TAPSOFT, volume 352 of Lecture Notes in Computer Science, pages 369\u2013383, Barcelona, March 1989. Springer-Verlag."},{"issue":"2","key":"8_CR17","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"25","author":"A. Tarski","year":"1955","unstructured":"A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 25(2):285\u2013309, 1955.","journal-title":"Pacific Journal of Mathematics"},{"key":"8_CR18","first-page":"501","volume-title":"volume 164 of Lecture Notes in Computer Science","author":"M. Vardi","year":"1983","unstructured":"M. Vardi and P. Wolper. Yet another process logic. In E.M. Clarke and D. Kozen, editors, Workshop on Logics of Programs, volume 164 of Lecture Notes in Computer Science, pages 501\u2013512, Pittsburgh, June 1983. SV."},{"key":"8_CR19","first-page":"332","volume-title":"An automata-theoretic approach to automatic program verification","author":"M. Vardi","year":"1986","unstructured":"M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Symposium on Logic in Computer Science (LICS '86), pages 332\u2013344, Cambridge, Massachusetts, June 1986. IEEE Computer Society Press."},{"key":"8_CR20","first-page":"761","volume-title":"Automata, Languages and Programming (ICALP '89), volume 372 of Lecture Notes in Computer Science","author":"G. Winskel","year":"1989","unstructured":"G. Winskel. A note on model checking the modal \u039d-calculus. In G. Ausiello, M. Dezani-Ciancaglini, and S. Ronchi Della Rocca, editors, Automata, Languages and Programming (ICALP '89), volume 372 of Lecture Notes in Computer Science, pages 761\u2013772, Stresa, Italy, July 1989. Springer-Verlag."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61042-1_41.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:28:50Z","timestamp":1619573330000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61042-1_41"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540610427","9783540498742"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-61042-1_41","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}