{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T10:59:15Z","timestamp":1775818755528,"version":"3.50.1"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[1996,8,1]],"date-time":"1996-08-01T00:00:00Z","timestamp":838857600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1996,8]]},"DOI":"10.1007\/bf00625970","type":"journal-article","created":{"date-parts":[[2004,11,30]],"date-time":"2004-11-30T17:17:52Z","timestamp":1101835072000},"page":"105-131","source":"Crossref","is-referenced-by-count":212,"title":["Symmetry and model checking"],"prefix":"10.1007","volume":"9","author":[{"given":"E. Allen","family":"Emerson","sequence":"first","affiliation":[]},{"given":"A. Prasad","family":"Sistla","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","unstructured":"S. Aggarwal, R.P. Kurshan, and K.K. Sabnani, ?A calculus for protocol specification and validation,? inProtocol Specification, Testing and Verification III, H. Ruden and C. West (Eds.), North-Holland, 1983, pp. 19?34."},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"P.C. Attie and E.A. Emerson, ?Synthesis of concurrent systems with many similar sequential processes,?Proc. 16th Annual ACM Symp. on Principles of Programming Languages, Austin, pp. 191?201, 1989.","DOI":"10.1145\/75277.75294"},{"key":"CR3","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M.C. Browne","year":"1988","unstructured":"M.C. Browne, E.M. Clarke, and O. Grumberg, ?Characterizing Kripke structures in temporal logic,?Theoretical Computer Science, Vol. 59, pp. 115?131, 1988.","journal-title":"Theoretical Computer Science"},{"issue":"No. 1","key":"CR4","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1016\/0890-5401(89)90026-6","volume":"81","author":"M.C. Browne","year":"1989","unstructured":"M.C. Browne, E.M. Clarke, and O. Grumberg, ?Reasoning about many identical processes,?Inform. and Comp., Vol. 81, No. 1, pp. 13?31, 1989.","journal-title":"Inform. and Comp."},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"E.M. Clarke and E.A. Emerson, ?Design and synthesis of synchronization skeletons using branching time temporal logic,? inProc. of the Workshop on Logics of Programs, Yorktown Heights and D. Kozen (Eds.), LNCS#131, Springer-Verlag, pp. 52?71, May 1981.","DOI":"10.1007\/BFb0025774"},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla, ?Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach,?, inProc. 10th Annual ACM Symp. on Principles of Programming Languages, Austin, 1983, pp. 117?126; also appeared inACM Transactions on Programming Languages and Systems, Vol. 8, No. 2, pp. 244?263, 1986.","DOI":"10.1145\/5397.5399"},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, T. Filkorn, and S. Jha, ?Exploiting symmetry in temporal logic model checking,? inProc. of 5th International Conference on Computer Aided Verification, Elounda, Greece, June 1993, pp. 450?462.","DOI":"10.1007\/3-540-56922-7_37"},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"S. Duri, U. Buy, R. Devarapalli, and S. Shatz, ?Using state space methods for deadlock analysis in ADA tasking,? in ACMProceedings of the 1993 International Symposium on Software Testing and Analysis, June 1993, pp. 51?60.","DOI":"10.1145\/174146.154197"},{"key":"CR9","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E.A. Emerson","year":"1982","unstructured":"E.A. Emerson and E.M. Clarke, ?Using branching time temporal logic to synthesize synchronization skeletons,?Science of Computer Programming, Vol. 2, pp. 241?266, 1982.","journal-title":"Science of Computer Programming"},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"E.A. Emerson, ?Temporal and modal logic,? inHandbook of Theoretical Computer Science, Vol. B:Formal Models and Semantics, J. van Leeuwen (Ed.), Elsevier Science Publishers, pp. 995?1072, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"CR11","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1016\/S0019-9958(84)80047-9","volume":"61","author":"E.A. Emerson","year":"1984","unstructured":"E.A. Emerson and A.P. Sistla, ?Deciding full branching time logic,?Information and Control, Vol. 61, pp. 175?201, 1984.","journal-title":"Information and Control"},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and A.P. Sistla, ?Symmetry and model checking,? inProc. of 5th International Conference on Computer Aided Verification, Elounda, Greece, June 1993, pp. 463?478.","DOI":"10.1007\/3-540-56922-7_38"},{"key":"CR13","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and A.P Sistla, ?Utilizing symmetry when model checking under fairness assumptions,? University of Texas at Austin, Computer Sciences Tech. Report TR-94-17, April 1994.","DOI":"10.1007\/3-540-60045-0_59"},{"key":"CR14","unstructured":"I. Herstein,Topics in Algebra, Xerox, 1964."},{"key":"CR15","unstructured":"C. Hoffmann, ?Graph isomorphism and permutation groups,? Springer LNCS No. 132, 1982."},{"key":"CR16","unstructured":"C.-W.N. Ip and D.L. Dill, ?Better verification through symmetry,? inProc. 11th International Symposium on Computer Hardware Description Languages (CHDL), April 1993."},{"key":"CR17","doi-asserted-by":"crossref","unstructured":"K. Jensen and G. Rozenberg (Eds.),High-level Petri Nets: Theory and Application, Springer-Verlag, 1991.","DOI":"10.1007\/978-3-642-84524-6"},{"key":"CR18","unstructured":"Z. Kohavi,Switching and Finite Automata Theory, McGraw-Hill, 1978."},{"key":"CR19","unstructured":"R.P. Kurshan, ?Testing containment of omega-regular languages,? Bell Labs Tech. Report 1121-861010-33 (1986); conference version in R.P. Kurshan,Reducibility in Analysis of Coordination, LNCIS 103 (1987) Springer-Verlag, 19?39."},{"key":"CR20","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"R.P. Kurshan","year":"1994","unstructured":"R.P. Kurshan,Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach, Princeton University Press, Princeton, New Jersey, 1994."},{"key":"CR21","doi-asserted-by":"crossref","unstructured":"D. Lee and M. Yannakakis, ?Online minimization of transition systems,?24th ACM Symposium on Theory of Computing, Victoria, Canada, pp. 264?274, 1992.","DOI":"10.1145\/129712.129738"},{"key":"CR22","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli,Temporal Logic of Reactive and Concurrent Systems: Specification, Springer-Verlag, 1992.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"CR23","unstructured":"P.H. Starke, ?Reachability analysis of petri nets using symmetries,?Syst. Anal. Model. Simul., Akademic Verlag, Vol. 8, Nos. 4\/5, pp. 293?303, 1991."},{"key":"CR24","unstructured":"C. Stirling, ?Modal and temporal logics,? inHandbook of Logic in Computer Science, D. Gabbay (Ed.), pp. 1?85, Oxford, 1993."},{"key":"CR25","doi-asserted-by":"crossref","unstructured":"H. Weyl,Symmetry, Princeton Univ. Press, 1952.","DOI":"10.1515\/9781400874347"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00625970.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00625970\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00625970","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,30]],"date-time":"2023-04-30T16:21:38Z","timestamp":1682871698000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00625970"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,8]]},"references-count":25,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1996,8]]}},"alternative-id":["BF00625970"],"URL":"https:\/\/doi.org\/10.1007\/bf00625970","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,8]]}}}