{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:08:55Z","timestamp":1763467735508},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"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":[[2006,1]]},"DOI":"10.1007\/s10703-006-4341-z","type":"journal-article","created":{"date-parts":[[2006,2,9]],"date-time":"2006-02-09T00:15:00Z","timestamp":1139444100000},"page":"37-56","source":"Crossref","is-referenced-by-count":42,"title":["An Algorithm for Strongly Connected Component Analysis in n log n Symbolic Steps"],"prefix":"10.1007","volume":"28","author":[{"given":"Roderick","family":"Bloem","sequence":"first","affiliation":[]},{"given":"Harold N.","family":"Gabow","sequence":"additional","affiliation":[]},{"given":"Fabio","family":"Somenzi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4341_CR1","doi-asserted-by":"crossref","unstructured":"R.K. Brayton et al., VIS. In Formal Methods in Computer Aided Design, Springer-Verlag, Berlin, LNCS 1166, 1996, pp. 248\u2013256.","DOI":"10.1007\/BFb0031812"},{"key":"4341_CR2","doi-asserted-by":"crossref","unstructured":"R. Bloem, K. Ravi, and F. Somenzi, \u201cEfficient decision procedures for model checking of linear time logic properties,\u201d in N. Halbwachs and D. Peled (Eds.), Eleventh Conference on Computer Aided Verification (CAV'99), Springer-Verlag, Berlin, LNCS 1633, 1999, pp. 222\u2013235, .","DOI":"10.1007\/3-540-48683-6_21"},{"issue":"8","key":"4341_CR3","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant, \u201cGraph-based algorithms for Boolean function manipulation,\u201d IEEE Transactions on Computers, vol. C-35, No. 8, pp. 677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"4341_CR4","unstructured":"J.R. B\u00fcchi, \u201cOn a decision method in restricted second order arithmetic,\u201d in Proceedings of the 1960 International Congress on Logic, Methodology, and Philosophy of Science, Stanford University Press, 1962, pp 1\u201311."},{"issue":"2","key":"4341_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, \u201cAutomatic verification of finite state concurrent systems using temporal logic specifications,\u201d ACM Transaction on Programming Languages and Systems, Vol. 8, No. 2, pp. 244\u2013263, 1986.","journal-title":"ACM Transaction on Programming Languages and Systems"},{"key":"4341_CR6","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, K. McMillan, and X. Zhao, \u201cEfficient generation of counterexamples and witnesses in symbolic model checking,\u201d in Proceedings of the Design Automation Conference, San Francisco, CA, 1995, pp. 427\u2013432.","DOI":"10.1145\/217474.217565"},{"key":"4341_CR7","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"E.M. Clarke, O. Grumberg, and D.A. Peled, Model Checking, MIT Press, Cambridge, MA, 1999."},{"key":"4341_CR8","unstructured":"E.A. Emerson and C.-L. Lei, \u201cEfficient model checking in fragments of the propositional mu-calculus,\u201d in Proceedings of the First Annual Symposium of Logic in Computer Science, 1986, pp. 267\u2013278."},{"key":"4341_CR9","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1016\/0167-6423(87)90036-0","volume":"8","author":"E.A. Emerson","year":"1987","unstructured":"E.A. Emerson and C. Lei, \u201cModalities for model checking: Branching time logic strikes back,\u201d Science of Computer Programming, Vol. 8, pp. 275\u2013306, 1987.","journal-title":"Science of Computer Programming"},{"issue":"1","key":"4341_CR10","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/322234.322235","volume":"28","author":"S. Even","year":"1981","unstructured":"S. Even and Y. Shiloach, \u201cAn on-line edge-deletion problem,\u201d Journal of the Association for Computing Machinery, Vol. 28, No. 1, pp. 1\u20134, 1981.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"4341_CR11","unstructured":"R. Gentilini, C. Piazza, and A. Policriti, \u201cComputing strongly connected componenets in a linear number of symbolic steps, in Symposium on Discrete Algorithms, Baltimore, MD, 2003."},{"key":"4341_CR12","doi-asserted-by":"crossref","unstructured":"R.H. Hardin, Z. Har'El, and R.P. Kurshan, \u201cCOSPAN,\u201d in T. Henzinger and R. Alur (Eds.), Eighth Conference on Computer Aided Verification (CAV'96), Springer-Verlag, Berlin, LNCS 1102, 1996, pp. 423\u2013427.","DOI":"10.1007\/3-540-61474-5_94"},{"key":"4341_CR13","doi-asserted-by":"crossref","unstructured":"R.H. Hardin, R.P. Kurshan, S.K. Shukla, and M.Y. Vardi, \u201cA new heuristic for bad cycle detection using BDDs,\u201d in O. Grumberg (Eds.), Ninth Conference on Computer Aided Verification (CAV'97), Springer-Verlag, Berlin, LNCS 1254, 1997, pp. 268\u2013278.","DOI":"10.1007\/3-540-63166-6_27"},{"key":"4341_CR14","unstructured":"G.H. Hardy, J.E. Littlewood, and G. P\u00f3lya, Inequalities, Cambridge University Press, 1952."},{"key":"4341_CR15","doi-asserted-by":"crossref","unstructured":"R. Hojati, T.R. Shiple, R. Brayton, and R. Kurshan, \u201cA unified approach to language containment and fair CTL model checking,\u201d in Proceedings of the Design Automation Conference, 1993, pp. 475\u2013481.","DOI":"10.1145\/157485.164985"},{"key":"4341_CR16","doi-asserted-by":"crossref","unstructured":"M.R. Henzinger and J.A. Telle, \u201cFaster algorithms for the nonemptiness of Streett automata and for communication protocol pruning,\u201d in R. Karlsson and A. Lingas (Eds.), Algorithm Theory: SWAT'96, Springer-Verlag, Berlin, LNCS 1097, 1996, pp. 16\u201327.","DOI":"10.1007\/3-540-61422-2_117"},{"key":"4341_CR17","doi-asserted-by":"crossref","unstructured":"R. Hojati, H. Touati, R.P. Kurshan, and R. K. Brayton, \u201cEfficient \u03c9-regular language containment,\u201d in Computer Aided Verification, Montr\u00e9al, Canada, 1992, pp. 371\u2013382.","DOI":"10.1007\/3-540-56496-9_31"},{"key":"4341_CR18","doi-asserted-by":"crossref","unstructured":"Y. Kesten, A. Pnueli, and L.-O. Raviv, \u201cAlgorithmic verification of linear temporal logic specifications,\u201d in International Colloquium on Automata, Languages, and Programming (ICALP-98), Berlin, Springer, LNCS 1443, 1998, pp. 1\u201316.","DOI":"10.1007\/BFb0055036"},{"key":"4341_CR19","volume-title":"Computer-Aided Verification of Coordinating Processes","author":"R.P. Kurshan","year":"1994","unstructured":"R.P. Kurshan, Computer-Aided Verification of Coordinating Processes, Princeton University Press, Princeton, NJ, 1994."},{"key":"4341_CR20","unstructured":"K. McMillan, \u201cClass project on BDD-based verification,\u201d Private Communication, E.M. Clarke, 1987."},{"key":"4341_CR21","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1994","unstructured":"K.L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Boston, MA, 1994."},{"key":"4341_CR22","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, \u201cVerification of infinite state systems by compositional model checking,\u201d in Correct Hardware Design and Verification Methods (CHARME'99), Berlin, Springer-Verlag. LNCS 1703, 1999, pp. 219\u2013233.","DOI":"10.1007\/3-540-48153-2_17"},{"key":"4341_CR23","doi-asserted-by":"crossref","unstructured":"K. Ravi, R. Bloem, and F. Somenzi, \u201cA comparative study of symbolic algorithms for the computation of fair cycles,\u201d in W.A. Hunt, Jr. and S.D. Johnson (Eds.), Formal Methods in Computer Aided Design, Springer-Verlag, LNCS 1954, 2000, pp. 143\u2013160.","DOI":"10.1007\/3-540-40922-X_10"},{"key":"4341_CR24","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/S0019-9958(82)91258-X","volume":"54","author":"R.S. Streett","year":"1982","unstructured":"R.S. Streett, \u201cPropositional dynamic logic of looping and converse is elementarily decidable,\u201d Information and Control, Vol. 54, pp. 121\u2013141, 1982.","journal-title":"Information and Control"},{"key":"4341_CR25","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R. Tarjan","year":"1972","unstructured":"R. Tarjan, \u201cDepth first search and linear graph algorithms,\u201d SIAM journal on Computing, Vol. 1, pp. 146\u2013160, 1972.","journal-title":"SIAM journal on Computing"},{"issue":"1","key":"4341_CR26","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, \u201cTesting language containment for \u03c9-automata using BDD's,\u201d Information and Computation, Vol. 118, No. 1, pp. 101\u2013109, 1995.","journal-title":"Information and Computation"},{"key":"4341_CR27","unstructured":"A. Xie and P. A. Beerel, \u201cImplicit enumeration of strongly connected components,\u201d in Proceedings of the International Conference on Computer-Aided Design, San Jose, CA, 1999, pp 37\u201340."},{"issue":"10","key":"4341_CR28","doi-asserted-by":"crossref","first-page":"1225","DOI":"10.1109\/43.875347","volume":"19","author":"A. Xie","year":"2000","unstructured":"A. Xie and P. A. Beerel, \u201cImplicit enumeration of strongly connected components and an application to formal verification,\u201d IEEE Transactions on Computer-Aided Design, Vol. 19, No. 10, pp. 1225\u20131230, 2000.","journal-title":"IEEE Transactions on Computer-Aided Design"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-4341-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-006-4341-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-006-4341-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:01:02Z","timestamp":1559253662000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-006-4341-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,1]]},"references-count":28,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2006,1]]}},"alternative-id":["4341"],"URL":"https:\/\/doi.org\/10.1007\/s10703-006-4341-z","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,1]]}}}