{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:24:55Z","timestamp":1759638295029},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2007,12,8]],"date-time":"2007-12-08T00:00:00Z","timestamp":1197072000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Algorithmica"],"published-print":{"date-parts":[[2008,1]]},"DOI":"10.1007\/s00453-007-9079-5","type":"journal-article","created":{"date-parts":[[2007,12,7]],"date-time":"2007-12-07T19:39:56Z","timestamp":1197056396000},"page":"120-158","source":"Crossref","is-referenced-by-count":26,"title":["Symbolic Graphs: Linear Solutions to Connectivity Related Problems"],"prefix":"10.1007","volume":"50","author":[{"given":"Raffaella","family":"Gentilini","sequence":"first","affiliation":[]},{"given":"Carla","family":"Piazza","sequence":"additional","affiliation":[]},{"given":"Alberto","family":"Policriti","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2007,12,8]]},"reference":[{"key":"9079_CR1","volume-title":"The Design and Analysis of Computer Algorithms","author":"A.V. Aho","year":"1974","unstructured":"Aho, A.V., Hopcroft, J.E., Ullman, J.D.: The Design and Analysis of Computer Algorithms. Addison\u2013Wesley, Reading (1974)"},{"issue":"6","key":"9079_CR2","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1109\/TC.1978.1675141","volume":"C-27","author":"S.B. Akers","year":"1978","unstructured":"Akers, S.B.: Binary decision diagrams. IEEE Trans. Comput. C-27(6), 509\u2013516 (1978)","journal-title":"IEEE Trans. Comput."},{"key":"9079_CR3","unstructured":"Bloem, R.P.: Search Techniques and Automata for Symbolic Model Checking. University of Colorado (2001)"},{"key":"9079_CR4","series-title":"LNCS","first-page":"37","volume-title":"Proc. of Int. Conference on Formal Methods in Computer-Aided Design (FMCAD\u201900)","author":"R.P. Bloem","year":"2000","unstructured":"Bloem, R.P., Gabow, H.N., Somenzi, F.: An algorithm for strongly connected component analysis in nlog\u2009n symbolic steps. In: Hunt, W.A. Jr., Johnson, S.D. (eds.) Proc. of Int. Conference on Formal Methods in Computer-Aided Design (FMCAD\u201900). LNCS, vol.\u00a01954, pp.\u00a037\u201354. Springer, Berlin (2000)"},{"key":"9079_CR5","first-page":"1","volume":"28","author":"R.P. Bloem","year":"2005","unstructured":"Bloem, R.P., Gabow, H.N., Somenzi, F.: An algorithm for strongly connected component analysis in nlog\u2009n symbolic steps. Form. Methods Syst. Des. 28, 1\u201320 (2005)","journal-title":"Form. Methods Syst. Des."},{"issue":"9","key":"9079_CR6","doi-asserted-by":"crossref","first-page":"993","DOI":"10.1109\/12.537122","volume":"45","author":"B. Bollig","year":"1996","unstructured":"Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comput. 45(9), 993\u20131002 (1996)","journal-title":"IEEE Trans. Comput."},{"key":"9079_CR7","series-title":"LNCS","first-page":"96","volume-title":"Proc. of Int. Conference on Computer Aided Verification (CAV\u201992)","author":"A. Bouali","year":"1992","unstructured":"Bouali, A., de Simone, R.: Symbolic bisimulation minimization. In: von Bochmann, G., Probst, D.K. (eds.) Proc. of Int. Conference on Computer Aided Verification (CAV\u201992). LNCS, vol.\u00a0663, pp.\u00a096\u2013108. Springer, Berlin (1992)"},{"key":"9079_CR8","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/3-540-61474-5_95","volume-title":"Proc. of Int. Conference on Computer Aided Verification (CAV\u201996)","author":"R.K. Brayton","year":"1996","unstructured":"Brayton, R.K., Hachtel, G.D., Sangiovanni-Vincentelli, A., Somenzi, F., Aziz, A., Cheng, S.T., Edwards, S., Khatri, S., Kukimoto, Y., Pardo, A., Qadeer, S., Ranjan, R.K., Sarwary, S., Shiple, T.R., Swamy, G., Villa, T.: VIS: a system for verification and synthesis. In: Alur, R., Henzinger, T.A. (eds.) Proc. of Int. Conference on Computer Aided Verification (CAV\u201996). LNCS, vol.\u00a01102, pp.\u00a0428\u2013432. Springer, Berlin (1996)"},{"issue":"8","key":"9079_CR9","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. C-35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"issue":"3","key":"9079_CR10","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R.E. Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic boolean manipulation with ordered binary decision diagrams. ACM Comput. Surv. 24(3), 293\u2013318 (1992)","journal-title":"ACM Comput. Surv."},{"key":"9079_CR11","first-page":"1","volume-title":"Proc. of IEEE Symp. on Logic in Computer Science (LICS\u201990)","author":"J.R. Burch","year":"1990","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. In: Proc. of IEEE Symp. on Logic in Computer Science (LICS\u201990), pp.\u00a01\u201333. IEEE Computer Society, Los Alamitos (1990)"},{"key":"9079_CR12","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"9079_CR13","volume-title":"Introduction to Algorithms","author":"T.H. Cormen","year":"1990","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. MIT Press, Cambridge (1990)"},{"key":"9079_CR14","first-page":"103","volume":"3","author":"R. Drechsler","year":"2001","unstructured":"Drechsler, R., Sieling, D.: Binary decision diagrams in theory and practice. Softw. Tools Technol. Transf. 3, 103\u2013112 (2001)","journal-title":"Softw. Tools Technol. Transf."},{"key":"9079_CR15","first-page":"267","volume-title":"Proc. of IEEE Symp. on Logic in Comuter Science (LICS\u201986)","author":"E.A. Emerson","year":"1986","unstructured":"Emerson, E.A., Lei, C.L.: Efficient model checking in fragments of the propositional mu-calculus. In: Proc. of IEEE Symp. on Logic in Comuter Science (LICS\u201986), pp.\u00a0267\u2013278. IEEE Computer Society, Los Alamitos (1986)"},{"key":"9079_CR16","doi-asserted-by":"crossref","first-page":"1","DOI":"10.4086\/cjtcs.1999.005","volume":"47","author":"J. Feigenbaum","year":"1999","unstructured":"Feigenbaum, J., Kannan, S., Vardi, M.Y., Viswanathan, M.: The complexity of problems on graphs represented as OBDDs. Chic. J. Theor. Comput. Sci. 47, 1\u201325 (1999)","journal-title":"Chic. J. Theor. Comput. Sci."},{"key":"9079_CR17","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1007\/3-540-48153-2_29","volume-title":"Proc. of Correct Hardware Design and Verification Methods (CHARME\u201999)","author":"K. Fisler","year":"1999","unstructured":"Fisler, K., Vardi, M.Y.: Bisimulation and model checking. In: Pierre, L., Kropf, T. (eds.) Proc. of Correct Hardware Design and Verification Methods (CHARME\u201999). LNCS, vol.\u00a01703, pp.\u00a0338\u2013341. Springer, Berlin (1999)"},{"issue":"1","key":"9079_CR18","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1023\/A:1016091902809","volume":"21","author":"K. Fisler","year":"2002","unstructured":"Fisler, K., Vardi, M.Y.: Bisimulation minimization and symbolic model checking. Form. Methods Syst. Des. 21(1), 39\u201378 (2002)","journal-title":"Form. Methods Syst. Des."},{"key":"9079_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4886-6","volume-title":"Fairness","author":"N. Francez","year":"1986","unstructured":"Francez, N.: Fairness. Springer, Berlin (1986)"},{"key":"9079_CR20","first-page":"875","volume-title":"Handbook of combinatorics","author":"A. Frank","year":"1995","unstructured":"Frank, A.: Connectivity and network flows. In: Handbook of combinatorics, vol.\u00a01, pp. 875\u2013917. Elsevier, Amsterdam (1995)"},{"key":"9079_CR21","first-page":"163","volume-title":"Proc. of ACM Sym. on Principles of Programming Languages (POPL\u201980)","author":"D.M. Gabbay","year":"1980","unstructured":"Gabbay, D.M., Pnueli, A., Shelah, S., Stavi, J.: On the temporal basis of fairness. In: Proc. of ACM Sym. on Principles of Programming Languages (POPL\u201980), pp.\u00a0163\u2013173. ACM, New York (1980)"},{"key":"9079_CR22","series-title":"LNCS","first-page":"554","volume-title":"Proc. of Int. Symposium on Algorithms and Computation (ISAAC\u201903)","author":"R. Gentilini","year":"2003","unstructured":"Gentilini, R., Policriti, A.: Biconnectivity on symbolically represented graphs: a\u00a0linear solution. In: Proc. of Int. Symposium on Algorithms and Computation (ISAAC\u201903). LNCS, vol.\u00a02906, pp.\u00a0554\u2013564. Springer, Berlin (2003)"},{"key":"9079_CR23","first-page":"573","volume-title":"Proc. of Int. Symposium on Discrete Algorithms (SODA\u201903)","author":"R. Gentilini","year":"2003","unstructured":"Gentilini, R., Piazza, C., Policriti, A.: Computing strongly connected components in a linear number of symbolic steps. In: Proc. of Int. Symposium on Discrete Algorithms (SODA\u201903), pp.\u00a0573\u2013582. ACM, New York (2003)"},{"issue":"2\/3","key":"9079_CR24","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1023\/A:1008651924240","volume":"10","author":"G.D. Hachtel","year":"1997","unstructured":"Hachtel, G.D., Somenzi, F.: A\u00a0symbolic algorithms for maximum flow in 0-1 networks. Form. Methods Syst. Des. 10(2\/3), 207\u2013219 (1997)","journal-title":"Form. Methods Syst. Des."},{"key":"9079_CR25","series-title":"LNCS","first-page":"396","volume-title":"Proc of Int. Conference on Computer Aided Verification (CAV\u201992)","author":"R. Hojati","year":"1992","unstructured":"Hojati, R., Touati, H.J., Kurshan, R.P., Brayton, R.K.: Efficient mega-regular language containment. In: von Bochmann, G., Probst, D.K. (eds.) Proc of Int. Conference on Computer Aided Verification (CAV\u201992). LNCS, vol.\u00a0663, pp.\u00a0396\u2013409. Springer, Berlin (1992)"},{"issue":"6","key":"9079_CR26","doi-asserted-by":"crossref","first-page":"372","DOI":"10.1145\/362248.362272","volume":"16","author":"J.E. Hopcroft","year":"1973","unstructured":"Hopcroft, J.E., Tarjan, R.E.: Efficient algorithms for graph manipulation [h] (algorithm 447). Commun. ACM 16(6), 372\u2013378 (1973)","journal-title":"Commun. ACM"},{"key":"9079_CR27","doi-asserted-by":"crossref","first-page":"985","DOI":"10.1002\/j.1538-7305.1959.tb01585.x","volume":"38","author":"C.Y. Lei","year":"1959","unstructured":"Lei, C.Y.: Representation of switching circuits by binary-decision programs. Bell Syst. Tech. J. 38, 985\u2013999 (1959)","journal-title":"Bell Syst. Tech. J."},{"key":"9079_CR28","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking: An Approach to the State Explosion Problem","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic, Dordrecht (1993)"},{"key":"9079_CR29","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-58940-9","volume-title":"Algorithms and Data Structures in VLSI Design. OBDD\u2014Foundations and Applications","author":"C. Meinel","year":"1998","unstructured":"Meinel, C., Theobald, T.: Algorithms and Data Structures in VLSI Design. OBDD\u2014Foundations and Applications. Springer, Berlin (1998)"},{"key":"9079_CR30","series-title":"LNCS","first-page":"1132","volume-title":"Proc. of Int. Symposium on Algorithms and Computation (ISAAC\u201905)","author":"R. Nunkesser","year":"2005","unstructured":"Nunkesser, R., Woelfel, P.: Representation of Graphs by OBDDs. In: Proc. of Int. Symposium on Algorithms and Computation (ISAAC\u201905). LNCS, vol.\u00a03827, pp.\u00a01132\u20131142. Springer, Berlin (2005)"},{"key":"9079_CR31","series-title":"LNCS","first-page":"143","volume-title":"Proc. of Int. Conference on Formal Methods in Computer-Aided Design (FMCAD\u201900)","author":"K. Ravi","year":"2000","unstructured":"Ravi, K., Bloem, R.P., Somenzi, F.: A comparative study of symbolic algorithms for the computation of fair cycles. In: Hunt, W.A. Jr., Johnson, S.D. (eds.) Proc. of Int. Conference on Formal Methods in Computer-Aided Design (FMCAD\u201900). LNCS, vol.\u00a01954, pp.\u00a0143\u2013160. Springer, Berlin (2000)"},{"key":"9079_CR32","unstructured":"Sanghavi, J.V., Ranjan, R.K., Brayton, R.K., Sangiovanni-Vincentelli, A.: High performance BDD package based on exploiting memory hierarchy. In: Proc. of ACM\/IEEE Design Automation Conference, 1996"},{"key":"9079_CR33","series-title":"LNCS","first-page":"301","volume-title":"Proc. of Int. Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM2004)","author":"D. Sawitzki","year":"2004","unstructured":"Sawitzki, D.: Implicit flow maximization by iterative squaring. In: Proc. of Int. Conference on Current Trends in Theory and Practice of Computer Science (SOFSEM2004). LNCS, vol.\u00a02932, pp.\u00a0301\u2013313. Springer, Berlin (2004)"},{"key":"9079_CR34","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/978-3-540-30559-0_13","volume-title":"Proc. of Int. Conference on Graph-Theoretic Concepts in Computer Science (WG 2004)","author":"D. Sawitzki","year":"2004","unstructured":"Sawitzki, D.: A symbolic approach to the all-pairs shortest-paths problem. In: Proc. of Int. Conference on Graph-Theoretic Concepts in Computer Science (WG 2004). LNCS, vol.\u00a03357, pp.\u00a0154\u2013167. Springer, Berlin (2004)"},{"key":"9079_CR35","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-10778-2","volume-title":"Verification of Reactive Systems","author":"K. Schneider","year":"2004","unstructured":"Schneider, K.: Verification of Reactive Systems. Springer, Berlin (2004)"},{"issue":"2","key":"9079_CR36","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1006\/inco.2001.3076","volume":"172","author":"D. Sieling","year":"2002","unstructured":"Sieling, D.: The nonapproximability of OBDD minimization. Inf. Comput. 172(2), 103\u2013138 (2002)","journal-title":"Inf. Comput."},{"key":"9079_CR37","series-title":"Nato Science Series F: Computer and Systems Sciences","first-page":"303","volume-title":"Calculational System Design","author":"F. Somenzi","year":"1999","unstructured":"Somenzi, F.: Binary decision diagrams. In: Calculational System Design, Nato Science Series F: Computer and Systems Sciences, vol.\u00a0173, pp.\u00a0303\u2013366. IOS Press, Amsterdam (1999)"},{"key":"9079_CR38","unstructured":"Somenzi, F.: CUDD: CU Decision Diagram Package Release 2.3.1 (2001). Available at http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/cuddIntro.html"},{"issue":"2","key":"9079_CR39","doi-asserted-by":"crossref","first-page":"146","DOI":"10.1137\/0201010","volume":"1","author":"R.E. Tarjan","year":"1972","unstructured":"Tarjan, R.E.: Depth first search and linear graph algorithms. SIAM J. Comput. 1(2), 146\u2013160 (1972)","journal-title":"SIAM J. Comput."},{"key":"9079_CR40","first-page":"133","volume-title":"Handbook of Theoretical Computer Science","author":"W. Thomas","year":"1990","unstructured":"Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, vol.\u00a0B, pp.\u00a0133\u2013191. MIT Press, Cambridge (1990)"},{"issue":"1","key":"9079_CR41","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1006\/inco.1995.1055","volume":"118","author":"J.H. Touati","year":"1995","unstructured":"Touati, J.H., Brayton, R.K., Kurshan, R.P.: Testing language containment for omega-automata using BDD\u2019s. Inf. Comput. 118(1), 101\u2013109 (1995)","journal-title":"Inf. Comput."},{"key":"9079_CR42","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency: Structure versus Automata","author":"M.Y. Vardi","year":"1996","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Logics for Concurrency: Structure versus Automata. LNCS, vol.\u00a01043, pp.\u00a0238\u2013266. Springer, Berlin (1996)"},{"key":"9079_CR43","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1016\/S0166-218X(03)00297-X","volume":"138","author":"I. Wegener","year":"2004","unstructured":"Wegener, I.: BDDs design, analysis, complexity, and applications. Discrete Appl. Math. 138, 229\u2013251 (2004)","journal-title":"Discrete Appl. Math."},{"key":"9079_CR44","doi-asserted-by":"crossref","unstructured":"Woelfel, R.: Symbolic topological sorting with OBDDs. J.\u00a0Discrete Algorithms (2006, to appear) (also in MFCS\u201903, LNCS, vol.\u00a02747, pp.\u00a0671\u2013680)","DOI":"10.1007\/978-3-540-45138-9_61"},{"key":"9079_CR45","doi-asserted-by":"crossref","first-page":"1225","DOI":"10.1109\/43.875347","volume":"19","author":"A. Xie","year":"2000","unstructured":"Xie, A., Beerel, P.: Implicit enumeration of strongly connected components and an application to formal verification. IEEE Trans. Comput. Aided Design Integrated Circuits Syst. 19, 1225\u20131230 (2000)","journal-title":"IEEE Trans. Comput. Aided Design Integrated Circuits Syst."},{"key":"9079_CR46","volume-title":"Proc. of IEEE First Workshop on Broadband Advanced Sensor Networks","author":"L. Yuan","year":"2003","unstructured":"Yuan, L., Gui, C., Chuah, C., Mohapatra, P.: Applications and design of heterogeneous and or broadband sensor networks. In: Proc. of IEEE First Workshop on Broadband Advanced Sensor Networks. IEEE Press, New York (2003)"}],"container-title":["Algorithmica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00453-007-9079-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00453-007-9079-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00453-007-9079-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T13:45:00Z","timestamp":1559137500000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00453-007-9079-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,12,8]]},"references-count":46,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2008,1]]}},"alternative-id":["9079"],"URL":"https:\/\/doi.org\/10.1007\/s00453-007-9079-5","relation":{},"ISSN":["0178-4617","1432-0541"],"issn-type":[{"value":"0178-4617","type":"print"},{"value":"1432-0541","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,12,8]]}}}