{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T10:18:59Z","timestamp":1773656339879,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540665595","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/3-540-48153-2_12","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:13:28Z","timestamp":1269897208000},"page":"142-157","source":"Crossref","is-referenced-by-count":59,"title":["From Asymmetry to Full Symmetry: New Techniques for Symmetry Reduction in Model Checking"],"prefix":"10.1007","author":[{"given":"E. Allen","family":"Emerson","sequence":"first","affiliation":[]},{"given":"Richard J.","family":"Trefler","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Lect Notes Comput Sci","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, 4th Interntational Conference, ETAPS98","author":"K. Ajami","year":"1998","unstructured":"Ajami, K., Haddad, S. and Ilie, J.-M., Exploiting Symmetry in Linear Time Temporal Logic Model Checking: One Step Beyond. In Tools and Algorithms for the Construction and Analysis of Systems, 4th Interntational Conference, ETAPS98 LNCS 1384, Springer Verlag, 1998."},{"issue":"2","key":"12_CR2","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. R. Burch","year":"1992","unstructured":"Burch, J. R., Clarke, E. M., McMillan, K. L., Dill, D. L. and Hwang, L. J., Symbolic Model Checking: 102 states and beyond. In Information and Computation, 98(2):142\u2013170, June, 1992.","journal-title":"Information and Computation"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Bryant, R. E., Graph-Based Algorithms for Boolean Function Manipulation. In IEEE Transactions on Computers, Vol. C-35, No. 8, Aug. 86, pp. 677\u2013691.","DOI":"10.1109\/TC.1986.1676819"},{"key":"12_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs Workshop","author":"E. M. Clarke","year":"1981","unstructured":"Clarke, E. M., and Emerson, E. A., Design and Verification of Synchronization Skeletons using Branching Time Temporal Logic. In Logics of Programs Workshop, Springer, LNCS no. 131., pp. 52\u201371, May 1981."},{"key":"12_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028741","volume-title":"Computer Aided Verification, 10th International Conference","author":"E. M. Clarke","year":"1998","unstructured":"Clarke, E. M., Emerson, E. A., Jha, S. and Sistla A. P., Symmetry Reductions in Model Checking. In Computer Aided Verification, 10th International Conference LNCS 1427, Springer-Verlag, 1998."},{"key":"12_CR6","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E. M. Clarke","year":"1986","unstructured":"Clarke, E. M., Emerson, E. A., and Sistla, A. P., Automatic Verification of Finite State Concurrent System Using Temporal Logic. In ACM Trans. on Prog. Lang. and Sys., vol. 8, no. 2, pp. 244\u2013263, April 1986.","journal-title":"ACM Trans. on Prog. Lang. and Sys."},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., Enders, R., Filkorn, T., and Jha, S., Exploiting Symmetry in Temporal Logic Model Checking. In Formal Methods in System Design, Kluwer, vol. 9, no. 1\/2, August 1996.","DOI":"10.1007\/BF00625969"},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Clarke, E. M., Grumberg, O. and Long, D. E., Model Checking and Abstraction. In Transactions on Programming Languages and Systems ACM, vol 16, no. 5, 1994.","DOI":"10.1145\/186025.186051"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"E. Allen Emerson, Temporal and Modal Logic. In J. van Leeuwen editor Handbook of Theoretical Computer Science vol. B, Elsevier Science Publishing, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Emerson, E. A., and Halpern, J. Y., \u2019sometimes\u2019 and \u2018Not Never\u2019 Revisited: On Branching versus Linear Time Temporal Logic, JACM, vol. 33, no. 1, pp. 151\u2013178, Jan. 86.","DOI":"10.1145\/4904.4999"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Emerson, E. A. and Sistla, A. P., Symmetry and Model Checking. In Formal Methods in System Design, Kluwer, vol. 9, no. 1\/2, August 1996.","DOI":"10.1007\/BF00625970"},{"issue":"4","key":"12_CR12","doi-asserted-by":"publisher","first-page":"617","DOI":"10.1145\/262004.262008","volume":"19","author":"E. A. Emerson","year":"1997","unstructured":"Emerson, E. A. and Sistla, A. P., Utilizing Symmetry when Model Checking under Fairness Assumptions. In TOPLAS 19(4): 617\u2013638 (1997).","journal-title":"TOPLAS"},{"key":"12_CR13","series-title":"Lect Notes Comput Sci","volume-title":"Mathematical Foundations of Computer Science, 23rd International Symposium","author":"E. A. Emerson","year":"1998","unstructured":"Emerson, E. A. and Trefler, R. J., Model Checking Real-Time Properties of Symmetric Systems. In Mathematical Foundations of Computer Science, 23rd International Symposium LNCS 1450, Springer-Verlag, 1998."},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Gyuris, V. and Sistla, A. P., On-the-Fly Model checking under Fairness that Exploits Symmetry. In Proceedings of the 9th International Conference on Computer Aided Verification, Haifa, Israel, 1997.","DOI":"10.1007\/3-540-63166-6_24"},{"key":"12_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-61044-8","volume-title":"Application and Theory of Petri Nets 1995","author":"S. Haddad","year":"1995","unstructured":"Haddad, S., Ilie, J. M., Taghelit, M. and Zouari, B., Symbolic Reachability Graph and Partial Symmetries. In Application and Theory of Petri Nets 1995, Springer-Verlag, LNCS 935, 1995."},{"issue":"1","key":"12_CR16","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"Hennessy, M., Milner, R., Algebraic Laws for Nondeterminism and Concurrency. In Journal of the ACM, Vol 32, no. 1, January, 1985, pp 137\u2013161.","journal-title":"Journal of the ACM"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"Ip, C-W. N., Dill, D. L., Better Verification through Symmetry. In Formal Methods in System Design, Kluwer, vol. 9, no. 1\/2, August 1996.","DOI":"10.1007\/BF00625968"},{"key":"12_CR18","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":"12_CR19","volume-title":"Switching and Finite Automata Theory","author":"K. Zvi","year":"1978","unstructured":"Kohavi, Zvi, Switching and Finite Automata Theory, second edition, McGraw-Hill Book Company, New York, 1978."},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., and Pnueli, A., Checking That Finite State Concurrent Programs Satisfy Their Linear Specifications, POPL85, pp. 97\u2013107, Jan. 85.","DOI":"10.1145\/318593.318622"},{"key":"12_CR21","series-title":"Lect Notes Comput Sci","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, 96","author":"M. F","year":"1996","unstructured":"Michel, F., Azema, P. and Vernadat, F., Permutable Agents in Process Algebra. In Tools and Algorithms for the Construction and Analysis of Systems, 96, Springer Verlag, LNCS 1055, 1996."},{"key":"12_CR22","unstructured":"Milner, R., An Algebraic Definition of Simulations Between Programs. In Proceedings of the Second International Joint Conference on Artificial Intelligence, British Computer Society, 1971, pp 481\u2013489."},{"key":"12_CR23","doi-asserted-by":"crossref","unstructured":"McMillan, K. L., Symbolic Model Checking: An Approach to the State Explosion Problem, Ph.D. Thesis, Carnegie Mellon University, 1992.","DOI":"10.1007\/978-1-4615-3190-6_3"},{"key":"12_CR24","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BFb0017309","volume-title":"Theoretical Computer Science: 5th GI-Conference, Karlsruhe","author":"D. Park","year":"1981","unstructured":"Park, D., Concurrency and Automata on Infinite Sequences. In Theoretical Computer Science: 5th GI-Conference, Karlsruhe, Springer-Verlag, LNCS 104, pp 167\u2013183, 1981."},{"key":"12_CR25","series-title":"Lect Notes Comput Sci","first-page":"195","volume-title":"Proc. 5th Int. Symp. Prog.","author":"J. P. Queille","year":"1982","unstructured":"Queille, J. P., and Sifakis, J., Specification and verification of concurrent programs in CESAR, Proc. 5th Int. Symp. Prog., Springer LNCS no. 137, pp. 195\u2013220, 1982."}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"language":"en","deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T19:15:02Z","timestamp":1739992502000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48153-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540665595"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/3-540-48153-2_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}