{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,18]],"date-time":"2025-10-18T20:47:38Z","timestamp":1760820458759},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540569220"},{"type":"electronic","value":"9783540477877"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56922-7_39","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:54:45Z","timestamp":1330257285000},"page":"479-490","source":"Crossref","is-referenced-by-count":37,"title":["Generation of reduced models for checking fragments of CTL"],"prefix":"10.1007","author":[{"given":"Dennis","family":"Dams","sequence":"first","affiliation":[]},{"given":"Orna","family":"Grumberg","sequence":"additional","affiliation":[]},{"given":"Rob","family":"Gerth","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,27]]},"reference":[{"key":"39_CR1","unstructured":"S, Bensalem, A. Bouajjani, C. Loiseaux, and J. Sifakis. Property preserving simulations. In CAV'92."},{"issue":"3","key":"39_CR2","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1016\/0167-6423(92)90018-7","volume":"18","author":"A. Bouajjani","year":"1992","unstructured":"A. Bouajjani, J.-C. Fernandez, N. Halbwachs, P. Raymond, and C. Ratel. Minimal state graph generation. Science of Computer Programming, 18(3):247\u2013271, 1992.","journal-title":"Science of Computer Programming"},{"key":"39_CR3","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M. C. Brown","year":"1988","unstructured":"M.C. Brown, E.M. Clarke, and O. Grumberg. Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science, 59:115\u2013131, 1988.","journal-title":"Theoretical Computer Science"},{"key":"39_CR4","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking: 1020 states and beyond. In Proc. 5th LICS, 1990."},{"key":"39_CR5","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. In Proc. 19th POPL, 1992.","DOI":"10.1145\/143165.143235"},{"issue":"2","key":"39_CR6","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 finitestate 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":"39_CR7","unstructured":"O. Coudert, J.C. Madre, and C. Berthet. Verifying temporal properties of sequential machines without building their state diagram. In CAV'90."},{"key":"39_CR8","unstructured":"D.R. Dams and O. Grumberg. Abstract interpretation of reactive systems: Abstractions preserving ACTL*, ECTL* and CTL*. Technical report, Eindhoven University of Technology, Department of Computer Science, 1992."},{"key":"39_CR9","doi-asserted-by":"crossref","unstructured":"D.L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. ACM Distinguished Dissertations. MIT Press, 1989.","DOI":"10.7551\/mitpress\/6874.001.0001"},{"issue":"1","key":"39_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. 'sometimes\u2019 and \u2018Not Never\u2019 revisited: on branching time versus linear time temporal logic. J. of the ACM, 33(1):151\u2013178, 1986.","journal-title":"J. of the ACM"},{"key":"39_CR11","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and J. Srinivasan. Branching time temporal logic. In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, LNCS 354, Springer-Verlag, 1988.","DOI":"10.1007\/BFb0013022"},{"key":"39_CR12","doi-asserted-by":"crossref","unstructured":"R. Enders, F. Filkorn, and D. Taubner. Generating BDDs for symbolic model checking in CCS. In CAV'91.","DOI":"10.1007\/3-540-55179-4_20"},{"key":"39_CR13","doi-asserted-by":"crossref","unstructured":"P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. In CAV'91.","DOI":"10.1007\/3-540-55179-4_32"},{"key":"39_CR14","unstructured":"S. Graf and C. Loiseaux. A tool for symbolic program verification and abstraction. In these proceedings."},{"key":"39_CR15","unstructured":"S. Graf and B. Steffen. Compositional minimization of finite state processes. In CAV'90."},{"key":"39_CR16","doi-asserted-by":"crossref","unstructured":"O. Grumberg and D.E. Long. Model checking and modular verification. In CONCUR'91, LNCS 527, Springer-Verlag, 1991.","DOI":"10.1007\/3-540-54430-5_93"},{"key":"39_CR17","doi-asserted-by":"crossref","unstructured":"A.J. Hu, D.L. Dill, A.J. Drexler, and C. Han Yang. Higher-level specification and verification with BDDs. In CAV'92.","DOI":"10.1007\/3-540-56496-9_8"},{"key":"39_CR18","doi-asserted-by":"crossref","unstructured":"R. Janicki and M. Koutny. On some implementation of optimal simulations. In CAV'90.","DOI":"10.1090\/dimacs\/003\/17"},{"key":"39_CR19","doi-asserted-by":"crossref","unstructured":"R. Kaivola and A. Valmari. The weakest compositional semantic equivalence preserving nexttime-less linear temporal logic. In CONCUR'92, LNCS 630, Springer-Verlag, 1992.","DOI":"10.1007\/BFb0084793"},{"key":"39_CR20","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/BF02252682","volume":"6","author":"S. Katz","year":"1992","unstructured":"S. Katz and D. Peled. Verification of distributed programs using representative interleaving sequences. Distributed Computing, 6:107\u2013120, 1992.","journal-title":"Distributed Computing"},{"key":"39_CR21","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan. Analysis of discrete event coordination. In Proc. Workshop on Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, LNCS 430, Springer-Verlag, 1989.","DOI":"10.1007\/3-540-52559-9_74"},{"key":"39_CR22","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli. Checking that finite state concurrent programs satisfy their linear specification. In Proc. 12th POPL, 1985.","DOI":"10.1145\/318593.318622"},{"key":"39_CR23","doi-asserted-by":"crossref","unstructured":"K. McMillan. Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In CA V'92.","DOI":"10.1007\/3-540-56496-9_14"},{"key":"39_CR24","unstructured":"R. Milner. An algebraic definition of simulation between programs. In IJCAI'71."},{"issue":"6","key":"39_CR25","doi-asserted-by":"crossref","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"R. Paige","year":"1987","unstructured":"R. Paige and R. Tarjan. Three partition refinement algorithms. SIAM Journal on Computing, 16(6):973\u2013989, 1987.","journal-title":"SIAM Journal on Computing"},{"key":"39_CR26","doi-asserted-by":"crossref","unstructured":"D. Park. Concurrency and automata on infinite sequences. In Proc. 5th GI-Conf. on Theoretical Computer Science, LNCS 104, Springer-Verlag, 1981.","DOI":"10.1007\/BFb0017309"},{"key":"39_CR27","unstructured":"D.K. Probst and H.F. Li. Using partial-order semantics to avoid the state explosion problem in asynchronous systems. In CAV'90."},{"key":"39_CR28","unstructured":"J.P. Quielle and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proc. 5th Int. Symp. on Programming, LNCS 137, Springer-Verlag, 1981."},{"key":"39_CR29","unstructured":"G. Shurek and O. Grumberg. The modular framework of computer-aided verification: Motivation, solutions and evaluation criteria. In CAV'90."},{"key":"39_CR30","unstructured":"A. Valmari. A stubborn attack on state explosion. In CAV'90."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56922-7_39.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:07:17Z","timestamp":1605647237000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56922-7_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540569220","9783540477877"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-56922-7_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}