{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:29:45Z","timestamp":1755217785776,"version":"3.43.0"},"reference-count":14,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2001,3,1]],"date-time":"2001-03-01T00:00:00Z","timestamp":983404800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,3,1]],"date-time":"2001-03-01T00:00:00Z","timestamp":983404800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2001,3]]},"DOI":"10.1023\/a:1008727508722","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T11:37:32Z","timestamp":1040557052000},"page":"131-140","source":"Crossref","is-referenced-by-count":10,"title":["A New Heuristic for Bad Cycle Detection Using BDDs"],"prefix":"10.1007","volume":"18","author":[{"given":"R. H.","family":"Hardin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"R. P.","family":"Kurshan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S. K.","family":"Shukla","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M. Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"315469_CR1","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J.R. Burch","year":"1992","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang, Symbolic model checking: 1020 states and beyond,\u201d Information and Computation, Vol. 98, No. 2, pp. 142\u2013170, 1992.","journal-title":"Information and Computation"},{"issue":"2","key":"315469_CR2","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, \u201cAutomatic verifications of finite-state concurrent systems using temporal logic specifications,\u201d ACM Transactions on Programming Languages and Systems, Vol. 8, No. 2, pp. 244\u2013263, 1986.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"315469_CR3","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/BF01383878","volume":"2","author":"R. Cleaveland","year":"1993","unstructured":"R. Cleaveland, \u201cA linear-time model-checking algorithm for the alternation-free modal \u03bc-calculus,\u201d Formal Methods in System Design, Vol. 2, pp. 121\u2013147, 1993.","journal-title":"Formal Methods in System Design"},{"key":"315469_CR4","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/BFb0023737","volume":"531","author":"C. Courcoubetis","year":"1991","unstructured":"C. Courcoubetis, M.Y. Vardi, P. Wolper, and M. Yannakakis, \u201cMemory efficient algorithms for the verification of temporal properties,\u201d Lecture Notes in Computer Science, Vol. 531, pp. 233\u2013245, 1991.","journal-title":"Lecture Notes in Computer Science"},{"key":"315469_CR5","unstructured":"E.A. Emerson and C.L. Lei, \u201cEfficient model checking in fragments of the propositional modal mu-calculus,\u201d in Proceedings of LICS 1986, 1986, pp. 267\u2013278."},{"key":"315469_CR6","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/3-540-61474-5_94","volume":"1102","author":"R.H. Hardin","year":"1996","unstructured":"R.H. Hardin, Z. Har'El, and R.P. Kurshan, \u201cCOSPAN,\u201d Lecture Notes in Computer Science, 1102:423\u2013427, 1996.","journal-title":"Lecture Notes in Computer Science"},{"key":"315469_CR7","unstructured":"R.H. Hardin, R.P. Kurshan, K.L. McMillan, J.A. Reeds, and N. J.A. Sloane, \u201cEfficient regression verification,\u201d in IEE Proc. WODES'96, 1996, pp. 147\u2013150."},{"key":"315469_CR8","doi-asserted-by":"crossref","unstructured":"R. Hojati, H.J. Touati, R.K. Brayton, and R.P. Kurshan, \u201cEfficient \u03c9-regular language containment,\u201d in Proceedings of CAV 93, LNCS 663, 1993, pp. 396\u2013409.","DOI":"10.1007\/3-540-56496-9_31"},{"key":"315469_CR9","doi-asserted-by":"crossref","unstructured":"R.P. Kurshan, Computer Aided Verification of Coordinating processes: An Automata Theoretic Approach, Princeton University Press, 1994.","DOI":"10.1515\/9781400864041"},{"key":"315469_CR10","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli, \u201cChecking that finite state concurrent programs satisfy their linear specifications,\u201d in Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, ACM, ACM, January 1985, pp. 97\u2013107.","DOI":"10.1145\/318593.318622"},{"key":"315469_CR11","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"315469_CR12","unstructured":"H.J. Touati, R.K. Brayton, and R.P. Kurshan, \u201cTesting language containment for omega-automata using BDD's,\u201d in Proceedings of The 1991 International Workshop on Formal Methods in VLSI Design, January 1991."},{"issue":"1","key":"315469_CR13","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1006\/inco.1995.1055","volume":"118","author":"H.J. Touati","year":"1995","unstructured":"H.J. Touati, R.K. Brayton, and R.P. Kurshan, Testing language containment for \u03c9-automata using BDD's, Information and Computation, 118(1):101\u2013109, April 1995.","journal-title":"Information and Computation"},{"key":"315469_CR14","unstructured":"M.Y. Vardi and P. Wolper, \u201cAn automata-theoretic approach to automatic program verification,\u201d in Proceedings of the First Symposium on Logic in Computer Science, Cambridge, June 1986, pp. 322\u2013331."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008727508722.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008727508722\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008727508722.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T19:31:07Z","timestamp":1754422267000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008727508722"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,3]]},"references-count":14,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2001,3]]}},"alternative-id":["315469"],"URL":"https:\/\/doi.org\/10.1023\/a:1008727508722","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2001,3]]}}}