{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T02:29:10Z","timestamp":1761964150218},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540414131"},{"type":"electronic","value":"9783540444503"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44450-5_1","type":"book-chapter","created":{"date-parts":[[2007,8,16]],"date-time":"2007-08-16T08:26:08Z","timestamp":1187252768000},"page":"1-10","source":"Crossref","is-referenced-by-count":1,"title":["Model Checking: Theory into Practice"],"prefix":"10.1007","author":[{"given":"E. Allen","family":"Emerson","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2000,11,24]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"15","author":"K. Apt","year":"1986","unstructured":"K. Apt and D. Kozen. Limits for automatic verification of finite-state concurrent systems. Information Processing Letters, 15, pages 307\u2013309, 1986.","journal-title":"Information Processing Letters"},{"issue":"1","key":"1_CR2","first-page":"13","volume":"81","author":"M.C. Browne","year":"1989","unstructured":"M.C. Browne, E.M. Clarke and O. Grumberg. Reasoning about Networks with Many Identical Finite State Processes. Information and Control, 81(1), pages 13\u201331, April 1989.","journal-title":"Information and Control"},{"issue":"8","key":"1_CR3","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant, \u201cGraph-Based Algorithms for Boolean FunctionManipulation\u201d IEEE Transactions on Computers, 35(8): 677\u2013691 (1986).","journal-title":"IEEE Transactions on Computers"},{"key":"1_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic","author":"E. M. Clarke","year":"1982","unstructured":"E. M. Clarke and E. A. Emerson, \u201cDesign and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic\u201d, Logics of Programs Workshop, IBM Yorktown Heights, New York, Springer LNCS no. 131, pp. 52\u201371, 1981."},{"issue":"1\/2","key":"1_CR5","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"E. M. Clarke","year":"96","unstructured":"E. M. Clarke, R. Enders, T. Filkorn, S. Jha, \u201cExploiting Symmetry In Temporal Logic Model Checking\u201d, Formal Methods in System Design, vol. 9, no. 1\/2, pp. 77\u2013104, Aug. 96.","journal-title":"Formal Methods in System Design"},{"issue":"2","key":"1_CR6","doi-asserted-by":"publisher","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, \u201cAutomatic Verification of Finite-State Concurrent Systems Using Temporal Logic Specifications\u201d, ACM Trans. on Prog. Lang. and Sys (TOPLAS) 8(2): 244\u2013263 (1986).","journal-title":"ACM Trans. on Prog. Lang. and Sys (TOPLAS)"},{"key":"1_CR7","unstructured":"E. A. Emerson, Branching Time Temporal Logic and the Design of Correct Concurrent Programs, Ph.D. Dissertation, Harvard University, 1981."},{"issue":"3","key":"1_CR8","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E. A. Emerson","year":"1982","unstructured":"E. A. Emerson, E M. Clarke, \u201cUsing Branching Time Temporal Logic to Synthesize Synchronization Skeletons\u201d, Science of Computer Programming, 2(3): 241\u2013266(1982)","journal-title":"Science of Computer Programming"},{"issue":"1","key":"1_CR9","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"E. A. Emerson","year":"1986","unstructured":"E. A. Emerson, J. Y. Halpern: \u201c\u2019 sometimes\u2019 and \u2018Not Never\u2019 Revisited: On Branching versus Linear Time Temporal Logic\u201d, Journal of the Assoc. Comp. Mach. (JACM), 33(1): 151\u2013178( 1986).","journal-title":"Journal of the Assoc. Comp. Mach. (JACM)"},{"key":"1_CR10","unstructured":"E. A. Emerson, J. Havlicek, and R. J. Trefler, \u201cVirtual Symmetry\u201d, LICS\u201900, pp. 121\u2013132."},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and K.S. Namjoshi. Reasoning about Rings. In Conference Record of POPL\u2019 95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 85\u201394, 1995.","DOI":"10.1145\/199448.199468"},{"key":"1_CR12","series-title":"Lect Notes Comput Sci","volume-title":"Automatic Verification of Parameterized Synchronous Systems","author":"E.A. Emerson","year":"1996","unstructured":"E.A. Emerson and K.S. Namjoshi. Automatic Verification of Parameterized Synchronous Systems. In Computer Aided Verification, Proceedings of the 8th International Conference. LNCS, Springer-Verlag, 1996."},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and K. S. Namjoshi, \u2018Verification of Parameterized Bus Arbitration Protocol\u2019, Conference on Computer Aided Verification (CAV), pp. 452\u2013463, 1998.","DOI":"10.1007\/BFb0028766"},{"issue":"1\/2","key":"1_CR14","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BF00625970","volume":"9","author":"E.A. Emerson","year":"96","unstructured":"E.A. Emerson and A.P. Sistla,. Symmetry and Model Checking. In Formal Methods in System Design, vol. 9, no. 1\/2, pp. 105\u2013131, Aug. 96.","journal-title":"Formal Methods in System Design"},{"issue":"4","key":"1_CR15","doi-asserted-by":"publisher","first-page":"617","DOI":"10.1145\/262004.262008","volume":"19","author":"E. A. Emerson","year":"1997","unstructured":"E. A. Emerson and A. P. Sistla, \u2018Utilizing Symmetry when Model-Checking under Fairness Assumptions: An Automata-Theoretic Approach\u2019, ACM Trans. on Prog. Lang. and Systems (TOPLAS), pp. 617\u2013638, vol. 19, no. 4, July 1997.","journal-title":"ACM Trans. on Prog. Lang. and Systems (TOPLAS)"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and R. J. Trefler, \u201cModel Checking Real-Time Properties of Symmetric Systems\u201d, MFCS 1998: 427\u2013436.","DOI":"10.1007\/BFb0055792"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"E. A. Emerson, R. J. Trefler, \u201cFrom Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking\u201d, CHARME 1999: 142\u2013156.","DOI":"10.1007\/3-540-48153-2_12"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"S.M. German and A.P. Sistla. Reasoning about Systems with Many Processes. J. ACM,39(3), July 1992.","DOI":"10.1145\/146637.146681"},{"issue":"1\/2","key":"1_CR19","first-page":"41","volume":"9","author":"C. Ip","year":"1996","unstructured":"C. Ip and D. Dill. Better verification through symmetry. In Formal Methods in System Design, vol. 9, no. 1\/2, pp. 41\u201376, Aug. 1996.","journal-title":"Formal Methods in System Design"},{"key":"1_CR20","unstructured":"Kamp, J. A. W., \u201cTense Logic and the Theory of Linear Order\u2019, Ph.D. thesis, University of California, Los Angeles, 19868."},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"R. P. Kurshan, Computer Aided Verification, Princeton Univ. Press, 1994.","DOI":"10.1007\/978-1-4615-3556-0"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan and K. McMillan. A Structural Induction Theorem for Processes. In Proceedings of the Eight Annual ACM Symposium on Principles of Distributed Computing, pages 239\u2013247, 1989.","DOI":"10.1145\/72981.72998"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"B. Lubachevsky. An Approach to Automating the Verification of Compact Parallel Coordination Programs I.Acta Informatica 21, 1984.","DOI":"10.1007\/BF00289237"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"K. McMillan, Symbolic Model Checking, Ph.D. Dissertation, CMU, 1992.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"1_CR25","unstructured":"K. McMillan, Verification of Infinite State Systems by Compositional Model Checking, CHARME\u201999."},{"key":"1_CR26","doi-asserted-by":"crossref","unstructured":"M Pandey and R. E. Bryant, \u2018Exploiting Symmetry When Verifying Transitor-Level Circuits by Symbolic Trajectory Evaluation\u2019, CAV 1997: 244\u2013255.","DOI":"10.1007\/3-540-63166-6_25"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"A. Pnueli. The Temporal Logic of Programs. In Proceedings of the eighteenth Symposium on Foundations of Computer Science. 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"A. Pnueli, \u2018Verification Engineering: A Future Profession\u2019 (A. M. Turing Award Lecture), Sixteenth Annual ACM Symposium on Principles of Distributed Computing (PODC 1990), San Diego, August, 1997; http:\/\/www.wisdom.weizmann.ac.il\/~amir\/turing97.ps.gz","DOI":"10.1145\/259380.259407"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"F. Pong and M. Dubois. A New Approach for the Verification of Cache Coherence Protocols. IEEE Transactions on Parallel and Distributed Systems, August 1995.","DOI":"10.1109\/71.406955"},{"key":"1_CR30","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J.-P. Queille","year":"1982","unstructured":"J-P. Queille and J. Sifakis, \u2018Specification and Verification of Concurrent Systems in CESAR\u2019, International Symposium on Programming, Springer LNCS no. 137, pp 337\u2013351, 1982."},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"A. P. Sistla, Parameterized Verification of Linear Networks Using Automata as Invariants, CAV, 1997, 412\u2013423.","DOI":"10.1007\/3-540-63166-6_40"},{"key":"1_CR32","unstructured":"I. Vernier. Specification and Verification of Parameterized Parallel Programs. In Proceedings of the 8th International Symposium on Computer and Information Sciences, Istanbul, Turkey, pages 622\u2013625,1993."},{"key":"1_CR33","series-title":"Lect Notes Comput Sci","volume-title":"Automatic Verification Metods for Finite State Systems","author":"P. Wolper","year":"1989","unstructured":"P. Wolper and V. Lovinfosse. Verifying Properties of Large Sets of Processes with Network Invariants. In J. Sifakis(ed) Automatic Verification Metods for Finite State Systems, Springer-Verlag, LNCS 407, 1989."}],"container-title":["Lecture Notes in Computer Science","FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44450-5_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T04:16:56Z","timestamp":1556770616000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44450-5_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540414131","9783540444503"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-44450-5_1","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}