{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:46:22Z","timestamp":1754484382567},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540600459"},{"type":"electronic","value":"9783540494133"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60045-0_59","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:36:36Z","timestamp":1330277796000},"page":"309-324","source":"Crossref","is-referenced-by-count":20,"title":["Utilizing symmetry when model checking under fairness assumptions: An automata-theoretic approach"],"prefix":"10.1007","author":[{"given":"E. A.","family":"Emerson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A. P.","family":"Sistla","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"25_CR1","unstructured":"Aggarwal S., Kurshan R. P., Sabnani K. K., \u201cA Calculus for Protocol Specification and Validation\u201d, in Protocol Specification, Testing and Verification III, H. Ruden, C. West (ed's), North-Holland 1983, 19\u201334."},{"key":"25_CR2","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Fernandez, J, Halbwichs, N., Raymond, P., and Ratel, C., Minimal State Graph Generation, Science of Computer Programming, 1992.","DOI":"10.1016\/0167-6423(92)90018-7"},{"key":"25_CR3","unstructured":"Clarke, E. M., and Emerson, E. A., Design and Verification of Synchronization Skeletons using Branching Time Temporal Logic, Logics of Programs Workshop 1981, Springer LNCS no. 131."},{"key":"25_CR4","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., Emerson, E. A., and Sistla, A. P., Automatic Verification of Finite State Concurrent Programs using Temporal Logic: A Practical Approach, ACM TOPLAS, April 1986","DOI":"10.1145\/5397.5399"},{"key":"25_CR5","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., Filkorn, T., Jha, S. Exploiting Symmetry in Temporal Logic Model Checking, 5th International Conference on Computer Aided Verification, Crete, Greece, June 1993.","DOI":"10.1007\/3-540-56922-7_37"},{"key":"25_CR6","unstructured":"Clarke, E. M., Grumberg, O., and Brown, M., Characterizing Kripke Structures in Temporal Logic, Theor. Comp. Sci., 1988"},{"key":"25_CR7","unstructured":"Clarke, E. M., Grumberg, O., and Brown, M., Reasoning about Many Identical Processes, Inform. and Comp., 1989"},{"key":"25_CR8","first-page":"129","volume":"no. 693","author":"R. Cleaveland","year":"1993","unstructured":"Cleaveland, R., Analyzing Concurrent Systems using the Concurrency Workbench, Functional Programming, Concurrency, Simulation, and Automated Reasoning Springer LNCS no. 693, pp. 129\u2013144, 1993.","journal-title":"Springer LNCS"},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"Dams, D., Grumberg, O., and Gerth, R., Generation of Reduced Models for checking fragments of CTL, CAV93, Springer LNCS no. 697, 1993.","DOI":"10.1007\/3-540-56922-7_39"},{"key":"25_CR10","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E. A. Emerson","year":"1987","unstructured":"Emerson, E. A. and Lei, C.-L., Modalities for Model Checking: branching Time Strikes Back, Science of Computer Programming, v. 8, pp. 275\u2013306, 1987","journal-title":"Science of Computer Programming"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Emerson, E. A., and Sistla, A. P., Symmetry and Model Checking, 5th International Conference on Computer Aided Verification, Crete, Greece, June 1993","DOI":"10.1007\/3-540-56922-7_38"},{"key":"25_CR12","volume-title":"Handbook of Theoretical Computer Science","author":"E. A. Emerson","year":"1991","unstructured":"Emerson, E. A., Temporal and Modal Logic, in Handbook of Theoretical Computer Science, (J. van Leeuwen, ed.), Elsevier\/North-Holland, 1991."},{"key":"25_CR13","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4886-6","volume-title":"Fairness","author":"N. Francez","year":"1986","unstructured":"Francez, N., Fairness, Springer-Verlag, New York, 1986"},{"issue":"No3","key":"25_CR14","doi-asserted-by":"crossref","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S. M. German","year":"1992","unstructured":"German, S. M. and Sistla, A. P. Reasoning about Systems with many Processes, Journal of the ACM, July 1992, Vol 39, No 3, pp 675\u2013735.","journal-title":"Journal of the ACM"},{"key":"25_CR15","unstructured":"Ip, C-W. N., Dill, D. L., Better Verification through Symmetry, CHDL, April 1993."},{"key":"25_CR16","unstructured":"Jensen, K., Colored Petri Nets: Basic Concepts, Analysis Methods, and Practical Use, vol. 2: Analysis Methods, EATCS Monographs, Springer-Verlag, 1994."},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"Jensen,K., and Rozenberg,G. (eds.), High-level Petri Nets: Theory and Application, Springer-Verlag, 1991.","DOI":"10.1007\/978-3-642-84524-6"},{"key":"25_CR18","unstructured":"Kurshan, R. P., \u201cTesting Containmentof omega-regular Languages\u201d, Bell Labs Tech. Report 1121-861010-33 (1986); conference version in R. P. Kurshan, \u201cReducibility in Analysis of Coordination\u201d, LNCIS 103 (1987) Springer-Verlag 19\u201339."},{"key":"25_CR19","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"R. P. Kurshan","year":"1994","unstructured":"Kurshan, R. P., Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach Princeton University Press, Princeton, New Jersey 1994."},{"key":"25_CR20","unstructured":"Lee. D., and Yannakakis, M., On-Line Minimization of Transition Systems, STOC92."},{"key":"25_CR21","unstructured":"Litchtenstein, O., and Pnueli, A., Checking That Finite State Concurrent Programs Satisfy Their Linear Specifications, POPL85"},{"key":"25_CR22","doi-asserted-by":"crossref","unstructured":"Manna, Z. and Pnueli, A., Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, 1992","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"25_CR23","unstructured":"Sistla, A. P. and German, S. M., Reasoning with many Processes, Proceedings of the Symposium on Logic in Computer Science, Ithaca, New York, 1987"},{"key":"25_CR24","doi-asserted-by":"crossref","unstructured":"Streett, R., Propositional Dynamic Logic of Looping and Converse, PhD Thesis, MIT, 1981.","DOI":"10.1145\/800076.802492"},{"key":"25_CR25","unstructured":"Vardi, M., and Wolper, P., An Automata-Theoretic Framework for Modal Logics of Programs, STOC84"},{"key":"25_CR26","unstructured":"Vardi, M., and Wolper, P., An Automata-Theoretic Framework for Automatic Program Verification, LICS86."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60045-0_59.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:28:55Z","timestamp":1605648535000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60045-0_59"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540600459","9783540494133"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-60045-0_59","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}