{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T04:19:12Z","timestamp":1742617152039,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540564966"},{"type":"electronic","value":"9783540475729"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56496-9_19","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:12:36Z","timestamp":1330254756000},"page":"234-247","source":"Crossref","is-referenced-by-count":2,"title":["Automatic reduction in CTL compositional model checking"],"prefix":"10.1007","author":[{"given":"Thomas R.","family":"Shiple","sequence":"first","affiliation":[]},{"given":"Massimiliano","family":"Chiodo","sequence":"additional","affiliation":[]},{"given":"Alberto L.","family":"Sangiovanni-Vincentelli","sequence":"additional","affiliation":[]},{"given":"Robert K.","family":"Brayton","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"issue":"8","key":"19_CR1","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant, \u201cGraph-Based Algorithms for Boolean Function Manipulation,\u201d IEEE Trans. on Computers, C-35(8), pp. 677\u2013691, Aug. 1986.","journal-title":"IEEE Trans. on Computers"},{"key":"19_CR2","doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill, \u201cSequential Circuit Verification Using Symbolic Model Checking,\u201d in Proc. of 27th Design Automation Conference, pp. 46\u201351, June 1990.","DOI":"10.1145\/123186.123223"},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. M. Clarke, and D. E. Long, \u201cRepresenting Circuits More Efficiently in Symbolic Model Checking,\u201d in Proc. of 28th Design Automation Conference, pp. 403\u2013407, June 1991.","DOI":"10.1145\/127601.127702"},{"key":"19_CR4","volume-title":"Memorandum No. UCB\/ERL M92\/55","author":"M. Chiodo","year":"1992","unstructured":"M. Chiodo, T. R. Shiple, A. Sangiovanni-Vincentelli, and R. K. Brayton, \u201cAutomatic Reduction in CTL Compositional Model Checking,\u201d Memorandum No. UCB\/ERL M92\/55, Electronics Research Laboratory, College of Engineering, University of California, Berkeley, Jan. 1992."},{"issue":"2","key":"19_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 P. Sistla, \u201cAutomatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications,\u201d ACM Trans. Prog. Lang. Syst., 8(2), pp. 244\u2013263, 1986.","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, D. E. Long, and K. L. McMillan, \u2018Compositional Model Checking,\u2019 in Proc. of the 4th Annual Symposium on Logic in Computer Science, Asilomar, CA, June 1989.","DOI":"10.1109\/LICS.1989.39190"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, O. Grumberg and D. E. Long, \u201cModel Checking and Abstraction,\u201d in Proc. of Principles of Programming Languages, Jan. 1992.","DOI":"10.1145\/143165.143235"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"O. Coudert, C. Berthel, and J. C. Madre, \u201cVerification of Synchronous Sequential Machines Based on Symbolic Execution,\u201d in Lecture Notes in Computer Science: Automatic Verification Methods for Finite State Systems, vol. 407, editor J. Sifakis, Springer-Verlag, pp. 365\u2013373, June 1989.","DOI":"10.1007\/3-540-52148-8_30"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"S. Graf and B. Steffen, \u201cCompositional Minimization of Finite State Systems,\u201d in Lecture Notes in Computer Science: Proc. of the 1990 Workshop on Computer-Aided Verification, vol. 531, editors R. P. Kurshan and E. M. Clarke, Springer-Verlag, pp. 186\u2013196, June 1990.","DOI":"10.1007\/BFb0023732"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"O. Grumberg and D. E. Long, \u201cModel Checking and Modular Verification,\u201d in Lecture Notes in Computer Science: Proc. CONCUR '91: 2nd Inter. Conf. on Concurrency Theory, vol. 527, editors J. C. M. Baeten and J. F. Groote, Springer-Verlag, Aug. 1991.","DOI":"10.1007\/3-540-54430-5_93"},{"key":"19_CR11","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/B978-0-12-417750-5.50022-1","volume-title":"The Theory of Machines and Computation","author":"J. E. Hopcroft","year":"1971","unstructured":"J. E. Hopcroft, \u201cAn n log n Algorithm for Minimizing the States in a Finite Automaton,\u201d in The Theory of Machines and Computation, New York: Academic Press, pp. 189\u2013196, 1971."},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"R. P. Kurshan and K. L. McMillan, \u201cA Structural Induction Theorem for Processes,\u201d in Proc. of 8th ACM Symp. on Principles of Distributed Computing, Aug. 1989.","DOI":"10.1145\/72981.72998"},{"key":"19_CR13","unstructured":"R. P. Kurshan, \u201cAnalysis of Discrete Event Coordination,\u201d in Lecture Notes in Computer Science: Proc. REX Workshop on Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, vol. 430, editors J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, Springer-Verlag, May 1989."},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"E. M. Sentovich, K. J. Singh, C. Moon, H. Savoj, R. K. Brayton, and A. Sangiovanni-Vincentelli, \u201cSequential Circuit Design Using Synthesis and Optimization,\u201d in Proc. of International Conference on Computer Design, Oct. 1992.","DOI":"10.1109\/ICCD.1992.276282"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"H. J. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. Sangiovanni-Vincentelli, \u201cImplicit State Enumeration of Finite State Machines using BDDs,\u201d in Proc. of IEEE International Conference on Computer-Aided Design, pp. 130\u2013133, Nov. 1990.","DOI":"10.1109\/ICCAD.1990.129860"},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"P. Wolper and V. Lovinfosse, \u201cVerifying Properties of Large Sets of Processes with Network Invariants,\u201d in Lecture Notes in Computer Science: Automatic Verification Methods for Finite State Systems, vol. 407, editor J. Sifakis, Springer-Verlag, pp. 68\u201380, June 1989.","DOI":"10.1007\/3-540-52148-8_6"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56496-9_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T21:49:15Z","timestamp":1742593755000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56496-9_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540564966","9783540475729"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-56496-9_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}