{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,17]],"date-time":"2026-03-17T04:59:30Z","timestamp":1773723570247,"version":"3.50.1"},"reference-count":19,"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\/bf00625969","type":"journal-article","created":{"date-parts":[[2004,11,30]],"date-time":"2004-11-30T17:17:52Z","timestamp":1101835072000},"page":"77-104","source":"Crossref","is-referenced-by-count":205,"title":["Exploiting symmetry in temporal logic model checking"],"prefix":"10.1007","volume":"9","author":[{"given":"E. M.","family":"Clarke","sequence":"first","affiliation":[]},{"given":"R.","family":"Enders","sequence":"additional","affiliation":[]},{"given":"T.","family":"Filkorn","sequence":"additional","affiliation":[]},{"given":"S.","family":"Jha","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1016\/0304-3975(88)90098-9","volume":"59","author":"M. Browne","year":"1988","unstructured":"M. Browne, E. Clarke, and O. Grumberg, ?Characterizing finite Kripke structures in propositional temporal logic,?Theoretical Comput. Sci., Vol. 59, pp. 115?131, 1988.","journal-title":"Theoretical Comput. Sci."},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"R.E. Bryant, ?Graph-based algorithms for boolean function manipulation,?IEEE Trans. Comput., Vol. C-35, No. 8, 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"CR3","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and J. Hwang, ?Symbolic model checking: 1020 states and beyond,? inProc. 5th Ann. Symp. on Logic in Comput. Sci., IEEE Comp. Soc. Press, June 1990."},{"key":"CR4","unstructured":"L. Claesen (Ed.),Proc. 11th Int. Symp. on Comput. Hardware Description Lang. and their Applications, North-Holland, Apr. 1993."},{"issue":"No. 2","key":"CR5","doi-asserted-by":"crossref","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, ?Automatic verification of finite-state concurrent systems using temporal logic specifications,?ACM Trans. Prog. Lang. Syst., Vol. 8, No. 2, pp. 244?263, 1986.","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"CR6","unstructured":"E.M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D.E. Long, K.L. McMillan, and L.A. Ness, ?Verification of the Futurebus + cache coherence protocol,? to appear inProc. 11th Int. Symp. on Comput. Hardware Description Lang, and their Applications, Apr. 1993."},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and A.P. Sistla, ?Symmetry and model checking,? inProc. Fifth Workshop on Comput.-Aided Verification, C. Courcabetis (Ed.), June 1993.","DOI":"10.1007\/3-540-56922-7_38"},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"E. Felt, G. York, R. Brayton, and A.S. Vincentelli, ?Dynamic variable reordering for bdd minimiation,? inProc. EuroDAC, pp. 130?135, Sept. 1993.","DOI":"10.1109\/EURDAC.1993.410627"},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"M. Furst, J. Hopcroft, and E. Luks, ?Polynomial-time algorithms for permutations groups,? inProc. 21st Ann. Symp. on Found. of Comput. Sci., 1980.","DOI":"10.1109\/SFCS.1980.34"},{"key":"CR10","unstructured":"M. Garey and D. Johnson,Computers and Intractibility, W.H. Freeman and Company, 1979."},{"key":"CR11","doi-asserted-by":"crossref","unstructured":"P. Huber, A. Jensen, L. Jepsen, and K. Jensen, ?Towards reachability trees for high-level Petri nets,? inAdvances on Petri Nets, G. Rozenberg (Ed.), pp. 215?233, 1984.","DOI":"10.1007\/3-540-15204-0_13"},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"S.L. Hurst, D.M. Miller, and J.C. Muzio,Special Techniques in Digital Logic, Academic Press, Inc., 1985.","DOI":"10.1016\/0165-1684(85)90052-0"},{"key":"CR13","unstructured":"IEEE Computer Society,IEEE Standard for Futurebus +?Logical Protocol Specification, Mar. 1992. IEEE Standard 896.I-1991."},{"key":"CR14","unstructured":"C. Ip and D. Dill, ?Better verification through symmetry,? to appear inProc. 11th Int. Symp. on Compuct. Hardware Description Lang. and their Applications, Apr. 1993."},{"key":"CR15","unstructured":"R.P. Kurshan, ?Testing containment of ?-regular languages,? Technical Report 1121-861010-33-TM, Bell Laboratories, 1986."},{"key":"CR16","unstructured":"B. Lin and A.R. Newton, ?Efficient symbolic manipulation of equivalence relations and classes,? inProc. 1991 Int. Workshop on Format Methods in VLSI Design, Jan. 1991."},{"key":"CR17","unstructured":"K.L. McMillan and J. Schwalbe, ?Formal verification of the Gigamax cache consistency protocol,? inShared Memory Multiprocessing, N. Suzuki (Ed.), MIT Press, 1992."},{"key":"CR18","unstructured":"R. Rudell, ?Dynamic variable reordering for ordered binary decision diagrams,? inProc. IEEE ICCAD, pp. 42?47, Nov. 1993."},{"issue":"Nos. 4\/5","key":"CR19","first-page":"293","volume":"8","author":"P. Starke","year":"1991","unstructured":"P. Starke, ?Reachability analysis of petri nets using symmetries,?Syst. Anal. Model. Simul., Vol. 8, Nos. 4\/5, pp. 293?303, 1991.","journal-title":"Syst. Anal. Model. Simul."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00625969.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00625969\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00625969","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,20]],"date-time":"2024-12-20T22:05:48Z","timestamp":1734732348000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00625969"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996,8]]},"references-count":19,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[1996,8]]}},"alternative-id":["BF00625969"],"URL":"https:\/\/doi.org\/10.1007\/bf00625969","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996,8]]}}}