{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T15:33:32Z","timestamp":1775835212955,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540552536","type":"print"},{"value":"9783540468035","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55253-7_1","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T09:56:35Z","timestamp":1330250195000},"page":"1-19","source":"Crossref","is-referenced-by-count":25,"title":["Model checking and boolean graphs"],"prefix":"10.1007","author":[{"given":"Henrik Reif","family":"Andersen","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1016\/0020-0190(88)90029-4","volume":"29","author":"A. Arnold","year":"1988","unstructured":"Andr\u00e9 Arnold and Paul Crubille. A linear algorithm to solve fixed-point equations on transitions systems. Information Processing Letters, 29:57\u201366, 1988.","journal-title":"Information Processing Letters"},{"key":"1_CR2","unstructured":"Henrik Reif Andersen and Glynn Winskel. Compositional checking of satisfaction. In Larsen and Skou [LS91]. To appear."},{"key":"1_CR3","unstructured":"H. Beki\u0107. Definable operations in general algebras, and the theory of automata and flow charts. Lecture Notes in Computer Science, 177, 1984."},{"key":"1_CR4","doi-asserted-by":"crossref","first-page":"725","DOI":"10.1007\/BF00264284","volume":"27","author":"R. Cleaveland","year":"1990","unstructured":"Rance Cleaveland. Tableau-based model checking in the propositional mucalculus. Acta Informatica, 27:725\u2013747, 1990.","journal-title":"Acta Informatica"},{"key":"1_CR5","unstructured":"Thomas H. Cormen, Charles E. Leiserson, and Ronald L. Rivest. Introduction to Algorithms. McGraw-Hill, 1990."},{"key":"1_CR6","unstructured":"Rance Cleaveland, Joachim Parrow, and Bernhard Steffen. The Concurrency Workbench: A semantics based tool for the verification of concurrent systems. Technical Report ECS-LFCS-89-83, Laboratory for Foundations of Computer Science, Uni. of Edinburgh, August 1989."},{"key":"1_CR7","unstructured":"Rance Cleaveland and Bernhard Steffen. A linear-time model-checking algorithm for the alternation-free modal mu-calculus. In Larsen and Skou [LS91]. To appear."},{"key":"1_CR8","unstructured":"Mads Dam. Translating CTL* into the modal \u03bc-calculus. Technical Report ECS-LFCS-90-123, Laboratory for Foundations of Computer Science, Uni. of Edinburgh, November 1990."},{"issue":"3","key":"1_CR9","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"1","author":"William F. F. Dowling","year":"1984","unstructured":"William F. Dowling and Jean H. Gallier. Linear-time algorithms for testing the satisfiability of propositional Horn formulae. Journal of Logic Programming, 1 (3):267\u2013284, 1984.","journal-title":"Journal of Logic Programming"},{"key":"1_CR10","unstructured":"E. Allen Emerson and Chin-Luang Lei. Efficient model checking in fragments of the propositional mu-calculus. In Symposium on Logic in Computer Science, Proceedings, pages 267\u2013278. IEEE, 1986."},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Dexter Kozen. Results on the prepositional mu-calculus. Theoretical Computer Science, 27, 1983.","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"1_CR12","unstructured":"Kim G. Laxsen. Proof systems for Hennessy-Milner logic with recursion. In Proceedings of CAAP, 1988."},{"key":"1_CR13","unstructured":"Kim G. Larsen, J.C. Godskesen, and M. Zeeberg. TAV-Tools for Automatic Verification. Technical Report R 89-19, Aalborg Universitetscenter, 1989."},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Kim G. Larsen and Arne Skou, editors. Proceedings of the 3rd Workshop on Computer Aided Verification, Aalborg, LNCS. Springer-Verlag, July 1991. To appear.","DOI":"10.1007\/3-540-55179-4"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Kim G. Larsen and Liu Xinxin. Compositionality through an operational semantics of contexts. In M.S. Paterson, editor, Proceedings of ICALP, volume 443 of LNCS, pages 526\u2013539. Springer-Verlag, 1990.","DOI":"10.1007\/BFb0032056"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Colin Stirling and David Walker. Local model checking in the modal mucalculus. In Proceedings of TAPSOFT, 1989.","DOI":"10.1007\/3-540-50939-9_144"},{"issue":"2","key":"1_CR17","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"Alfred Tarski","year":"1955","unstructured":"A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5, 1955.","journal-title":"Pacific Journal of Mathematics"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Glynn Winskel. A note on model checking the modal v-calculus. In Ausiello, Dezani-Ciancaglini, and Rocca, editors, Proceedings of ICALP, volume 372 of LNCS, 1989.","DOI":"10.1007\/BFb0035797"}],"container-title":["Lecture Notes in Computer Science","ESOP '92"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55253-7_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T04:17:13Z","timestamp":1640924233000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55253-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540552536","9783540468035"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-55253-7_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992]]}}}