{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:01:11Z","timestamp":1725663671060},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540551799"},{"type":"electronic","value":"9783540467632"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55179-4_4","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T09:52:28Z","timestamp":1330249948000},"page":"24-36","source":"Crossref","is-referenced-by-count":5,"title":["Compositional checking of satisfaction"],"prefix":"10.1007","author":[{"given":"Henrik Reif","family":"Andersen","sequence":"first","affiliation":[]},{"given":"Glynn","family":"Winskel","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,29]]},"reference":[{"key":"4_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"},{"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":"4_CR2"},{"issue":"2","key":"4_CR3","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, 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"4_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 mu-calculus. Acta Informatica, 27:725\u2013747, 1990.","journal-title":"Acta Informatica"},{"doi-asserted-by":"crossref","unstructured":"E.M. Clarke, D.E. Long, and K.L. McMillan. Compositional model checking. In Procedings of 4th Annual Symposium on Logic in Computer Science. IEEE, 1989.","key":"4_CR5","DOI":"10.1109\/LICS.1989.39190"},{"unstructured":"Mads Dam. Translating CTL* into the modal \u039c-calculus. Technical Report ECS-LFCS-90-123, Laboratory for Foundations of Computer Science, Uni. of Edinburgh, November 1990.","key":"4_CR6"},{"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":"4_CR7"},{"unstructured":"Kim G. Larsen. Proof systems for Hennessy-Milner logic with recursion. In Proceedings of CAAP, 1988.","key":"4_CR8"},{"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, 1990.","key":"4_CR9"},{"unstructured":"Colin Stirling. Modal and Temporal Logics. In S. Abramsky, D. Gabbay, and T. Maibaum, editors, Handbook of Logic in Computer Science. Oxford University Press, 1991.","key":"4_CR10"},{"doi-asserted-by":"crossref","unstructured":"Colin Stirling and David Walker. Local model checking in the modal mu-calculus. In Proceedings of TAPSOFT, 1989.","key":"4_CR11","DOI":"10.1007\/3-540-50939-9_144"},{"doi-asserted-by":"crossref","unstructured":"A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5, 1955.","key":"4_CR12","DOI":"10.2140\/pjm.1955.5.285"},{"doi-asserted-by":"crossref","unstructured":"Glynn Winskel. A note on model checking the modal v-calculus. In Proceedings of ICALP, volume 372 of LNCS, 1989.","key":"4_CR13","DOI":"10.1007\/BFb0035797"},{"doi-asserted-by":"crossref","unstructured":"Glynn Winskel. On the compositional checking of validity. In J.C.M. Baeten and J.W. Klop, editors, Proceedings of CONCUR '90, volume 458 of LNCS, 1990.","key":"4_CR14","DOI":"10.1007\/BFb0039079"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55179-4_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:28:18Z","timestamp":1619573298000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55179-4_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540551799","9783540467632"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-55179-4_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}