{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:35:00Z","timestamp":1759638900225},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540474609"},{"type":"electronic","value":"9783540474623"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11901433_6","type":"book-chapter","created":{"date-parts":[[2006,11,20]],"date-time":"2006-11-20T12:40:51Z","timestamp":1164026451000},"page":"94-113","source":"Crossref","is-referenced-by-count":7,"title":["Reducing Model Checking of the Few to the One"],"prefix":"10.1007","author":[{"given":"E. Allen","family":"Emerson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Richard J.","family":"Trefler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Wahl","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Apt, K.R., Kozen, D.: Limits for automatic verification of finite-state concurrent systems. Information Processing Letters (IPL) (1986)","DOI":"10.1016\/0020-0190(86)90071-2"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without bdds. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, p. 193. Springer, Heidelberg (1999)"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-540-45187-7_11","volume-title":"CONCUR 2003 - Concurrency Theory","author":"A. Bouajjani","year":"2003","unstructured":"Bouajjani, A., Habermehl, P., Vojnar, T.: Verification of parametric concurrent systems with prioritized fifo resource management. In: Amadio, R., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol.\u00a02761, pp. 174\u2013190. Springer, Heidelberg (2003)"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers (1986)","DOI":"10.1109\/TC.1986.1676819"},{"key":"6_CR5","unstructured":"Clarke, E.M., Allen Emerson, E.: The design and synthesis of synchronization skeletons using temporal logic. In: Logic of Programs (LOP) (1981)"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Formal Methods in System Design (FMSD) (1996)","DOI":"10.1007\/BF00625969"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O.: Avoiding the state explosion problem in temporal logic model checking. In: Principles of Distributed Computing (PODC) (1987)","DOI":"10.1145\/41840.41865"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Browne, M.C.: Reasoning about networks with many identical finite-state processes. In: Principles of Distributed Computing (PODC) (1986)","DOI":"10.21236\/ADA188743"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-540-30494-4_27","volume-title":"Formal Methods in Computer-Aided Design","author":"C. Ching-Tsun","year":"2004","unstructured":"Ching-Tsun, C., Mannava, P.K., Seungjoon, P.: A simple method for parameterized verification of cache coherence protocols. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 382\u2013398. Springer, Heidelberg (2004)"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Allen Emerson, E., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming (SOCP) (1982)","DOI":"10.1016\/0167-6423(83)90017-5"},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"Allen Emerson, E., Kahlon, V.: Reducing model checking of the many to the few. In: Computer-Aided Design (CAD) (2000)","DOI":"10.1007\/10721959_19"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/3-540-46002-0_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E. Allen Emerson","year":"2002","unstructured":"Allen Emerson, E., Kahlon, V.: Model checking large-scale and parameterized resource allocation systems. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, p. 251. Springer, Heidelberg (2002)"},{"key":"6_CR13","unstructured":"Allen Emerson, E.: Temporal and model logic. In: Handbook of Theoretical Computer Science. North-Holland Pub. Co.\/MIT Press (1990)"},{"key":"6_CR14","series-title":"Lecture Notes in Computer Science","volume-title":"Computer Aided Verification","author":"E. Allen Emerson","year":"1996","unstructured":"Allen Emerson, E., Namjoshi, K.S.: Automatic verification of parameterized synchronous systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102. Springer, Heidelberg (1996)"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Allen Emerson, E., Prasad Sistla, A.: Symmetry and model checking. In: Formal Methods in System Design (FMSD) (1996)","DOI":"10.1007\/BF00625970"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/978-3-540-39724-3_20","volume-title":"Correct Hardware Design and Verification Methods","author":"E. Allen Emerson","year":"2003","unstructured":"Allen Emerson, E., Wahl, T.: On combining symmetry reduction and symbolic representation for efficient model checking. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 216\u2013230. Springer, Heidelberg (2003)"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"German, S.M., Prasad Sistla, A.: Reasoning about systems with many processes. Journal of the ACM (1992)","DOI":"10.1145\/146637.146681"},{"key":"6_CR18","unstructured":"Norris Ip, C., Dill, D.L.: Verifying systems with replicated components in Mur\u03c6. Formal Methods in System Design (FMSD) (1999)"},{"key":"6_CR19","unstructured":"Kumar, V., Grama, A., Gupta, A., Karypis, G.: Introduction to Parallel Computing. Benjamin\/Cummings Publishing (1994)"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Kurshan, R.P., McMillan, K.: A structural induction theorem for processes. In: Principles of distributed computing (PODC) (1989)","DOI":"10.1145\/72981.72998"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Lubachevsky, B.D.: An approach to automating the verification of compact parallel coordination programs. Acta Informatica (1984)","DOI":"10.1007\/3-540-12896-4_371"},{"key":"6_CR22","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking: An Approach to the State Explosion Problem","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic, Dordrecht (1993)"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Mellor-Crummey, J.M., Scott, M.L.: Algorithms for scalable synchronization on shared-memory multiprocessors. Transactions on Computer Systems (TOCS) (1991)","DOI":"10.1145\/109625.109637"},{"key":"6_CR24","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"Quielle, J.-P., Sifakis, J.: Specification and verification of concurrent systems in cesar. In: 5th International Symposium on Programming (1982)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"6_CR26","unstructured":"Somenzi, F.: The CU Decision Diagram Package, release 2.3.1. University of Colorado at Boulder, \n                    \n                      http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11901433_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T18:00:50Z","timestamp":1558288850000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11901433_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540474609","9783540474623"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/11901433_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}