{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:28:21Z","timestamp":1761611301364},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540603603"},{"type":"electronic","value":"9783540450504"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60360-3_32","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T13:20:08Z","timestamp":1330262408000},"page":"51-63","source":"Crossref","is-referenced-by-count":24,"title":["Optimality in abstractions of model checking"],"prefix":"10.1007","author":[{"given":"Rance","family":"Cleaveland","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Purush","family":"Iyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Yankelevich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"S. Bensalem, A. Bouajjani, C. Loiseaux and J. Sifakis. Property prerving simulations. In CAV 92, LNCS 663, 1992.","DOI":"10.1007\/3-540-56496-9_21"},{"key":"5_CR2","unstructured":"J. R. Burch, E. M. Clarke and D. E. Long. Symbolic model checking with partitioned transition relations. In VLSI 91, Edinburgh, Scotland, 1990."},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, O. Grumberg and D. Long. Model checking and abstraction. In Proc of XIX POPL, Jan 1992.","DOI":"10.1145\/143165.143235"},{"key":"5_CR4","unstructured":"R. Cleaveland, S. P. Iyer, D. Yankalevich. Abstractions for preserving all CTL* formulae Tech Report 94\u201303, NCSU Computer Science Department, 1994."},{"issue":"2","key":"5_CR5","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 TOPLAS, 8(2):244\u2013263, 1986.","journal-title":"ACM TOPLAS"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Systematic Design of Program Analysis Frameworks. In VI POPL, 1979.","DOI":"10.1145\/567752.567778"},{"key":"5_CR7","unstructured":"P. Cousot and R. Cousot. Comparing the Galois connection and the widening\/narrowing approaches to abstract interpretation. In Proc of Conference on Programming Language Implementation and Logic Programming, LNCS 631, August, 1992."},{"key":"5_CR8","unstructured":"D. Dams, O. Grumberg and R. Gerth. Abstract Interpretation of Reactive Systems: Abstractions Preserving \u2200CTL*, \u2203CTL* and CTL*. In IEEE PRO-COMONET. Nov, 1994."},{"issue":"1","key":"5_CR9","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. \u201cSometimes\u201d and \u201cnot never\u201d revisited: on branching time versus linear time temporal logic. JACM, 33(1):151\u2013178, 1986.","journal-title":"JACM"},{"key":"5_CR10","unstructured":"N. Jones and P. Nielsen. Abstract Interpretation: a Semantic-Based Tool for Program Analysis. To appear in Handbook of Logic in Computer Science, (ed) S. Abramsky, D. Gabbay and T. S. E. Maibaum."},{"key":"5_CR11","unstructured":"P. Kelb. Model Checking and Abstraction: A framework approximating both truth and failure information. University of Oldenburg, March 30, 1994."},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"K. Larsen. Modal Specifications. In Proc. of CAV '89, (ed) J. Sifakis, LNCS Vol. 407, pp: 232\u2013246, 1989.","DOI":"10.1007\/3-540-52148-8_19"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. Temporal Logic of Reactive and Concurrent Systems Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"J. P. Quielle and J. Sifakis. Specification and Verification of Concurrent Systems in Cesar. In Proc of V International Symposium on Programming, LNCS Vol 137, 1981.","DOI":"10.1007\/3-540-11494-7_22"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60360-3_32.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,20]],"date-time":"2023-06-20T14:59:17Z","timestamp":1687273157000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60360-3_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540603603","9783540450504"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-60360-3_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}