Abstract
The importance of symbolic data structures such as Ordered Binary Decision Diagrams (OBDD) is rapidly growing in many areas of Computer Science where the large dimensions of the input models is a challenging feature: OBDD based graph representations allowed to define truly new standards in the achievable dimensions for the Model Checking verification technique. However, OBDD representations pose strict constraints in the algorithm design issue. For example, Depth-First Search (DFS) is not feasible in a symbolic framework and, consequently, many state-of-the-art DFS based algorithms (e.g., connectivity procedures) cannot be easily rearranged to work on symbolically represented graphs. We devise here a symbolic algorithmic strategy, based on the new notion of spine-set, that is general enough to be the engine of linear symbolic step algorithms for both strongly connected components and biconnected components. Our procedures improve on previously designed connectivity symbolic algorithms. Moreover, by an application to the so-called “bad cycle detection problem”, our technique can be used to efficiently solve the emptiness problem for various kinds of ω-automata.
Similar content being viewed by others
References
Aho, A.V., Hopcroft, J.E., Ullman, J.D.: The Design and Analysis of Computer Algorithms. Addison–Wesley, Reading (1974)
Akers, S.B.: Binary decision diagrams. IEEE Trans. Comput. C-27(6), 509–516 (1978)
Bloem, R.P.: Search Techniques and Automata for Symbolic Model Checking. University of Colorado (2001)
Bloem, R.P., Gabow, H.N., Somenzi, F.: An algorithm for strongly connected component analysis in nlog n symbolic steps. In: Hunt, W.A. Jr., Johnson, S.D. (eds.) Proc. of Int. Conference on Formal Methods in Computer-Aided Design (FMCAD’00). LNCS, vol. 1954, pp. 37–54. Springer, Berlin (2000)
Bloem, R.P., Gabow, H.N., Somenzi, F.: An algorithm for strongly connected component analysis in nlog n symbolic steps. Form. Methods Syst. Des. 28, 1–20 (2005)
Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. Comput. 45(9), 993–1002 (1996)
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’92). LNCS, vol. 663, pp. 96–108. Springer, Berlin (1992)
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’96). LNCS, vol. 1102, pp. 428–432. Springer, Berlin (1996)
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. C-35(8), 677–691 (1986)
Bryant, R.E.: Symbolic boolean manipulation with ordered binary decision diagrams. ACM Comput. Surv. 24(3), 293–318 (1992)
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’90), pp. 1–33. IEEE Computer Society, Los Alamitos (1990)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. MIT Press, Cambridge (1990)
Drechsler, R., Sieling, D.: Binary decision diagrams in theory and practice. Softw. Tools Technol. Transf. 3, 103–112 (2001)
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’86), pp. 267–278. IEEE Computer Society, Los Alamitos (1986)
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–25 (1999)
Fisler, K., Vardi, M.Y.: Bisimulation and model checking. In: Pierre, L., Kropf, T. (eds.) Proc. of Correct Hardware Design and Verification Methods (CHARME’99). LNCS, vol. 1703, pp. 338–341. Springer, Berlin (1999)
Fisler, K., Vardi, M.Y.: Bisimulation minimization and symbolic model checking. Form. Methods Syst. Des. 21(1), 39–78 (2002)
Francez, N.: Fairness. Springer, Berlin (1986)
Frank, A.: Connectivity and network flows. In: Handbook of combinatorics, vol. 1, pp. 875–917. Elsevier, Amsterdam (1995)
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’80), pp. 163–173. ACM, New York (1980)
Gentilini, R., Policriti, A.: Biconnectivity on symbolically represented graphs: a linear solution. In: Proc. of Int. Symposium on Algorithms and Computation (ISAAC’03). LNCS, vol. 2906, pp. 554–564. Springer, Berlin (2003)
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’03), pp. 573–582. ACM, New York (2003)
Hachtel, G.D., Somenzi, F.: A symbolic algorithms for maximum flow in 0-1 networks. Form. Methods Syst. Des. 10(2/3), 207–219 (1997)
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’92). LNCS, vol. 663, pp. 396–409. Springer, Berlin (1992)
Hopcroft, J.E., Tarjan, R.E.: Efficient algorithms for graph manipulation [h] (algorithm 447). Commun. ACM 16(6), 372–378 (1973)
Lei, C.Y.: Representation of switching circuits by binary-decision programs. Bell Syst. Tech. J. 38, 985–999 (1959)
McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic, Dordrecht (1993)
Meinel, C., Theobald, T.: Algorithms and Data Structures in VLSI Design. OBDD—Foundations and Applications. Springer, Berlin (1998)
Nunkesser, R., Woelfel, P.: Representation of Graphs by OBDDs. In: Proc. of Int. Symposium on Algorithms and Computation (ISAAC’05). LNCS, vol. 3827, pp. 1132–1142. Springer, Berlin (2005)
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’00). LNCS, vol. 1954, pp. 143–160. Springer, Berlin (2000)
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
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. 2932, pp. 301–313. Springer, Berlin (2004)
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. 3357, pp. 154–167. Springer, Berlin (2004)
Schneider, K.: Verification of Reactive Systems. Springer, Berlin (2004)
Sieling, D.: The nonapproximability of OBDD minimization. Inf. Comput. 172(2), 103–138 (2002)
Somenzi, F.: Binary decision diagrams. In: Calculational System Design, Nato Science Series F: Computer and Systems Sciences, vol. 173, pp. 303–366. IOS Press, Amsterdam (1999)
Somenzi, F.: CUDD: CU Decision Diagram Package Release 2.3.1 (2001). Available at http://vlsi.colorado.edu/~fabio/CUDD/cuddIntro.html
Tarjan, R.E.: Depth first search and linear graph algorithms. SIAM J. Comput. 1(2), 146–160 (1972)
Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, vol. B, pp. 133–191. MIT Press, Cambridge (1990)
Touati, J.H., Brayton, R.K., Kurshan, R.P.: Testing language containment for omega-automata using BDD’s. Inf. Comput. 118(1), 101–109 (1995)
Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Logics for Concurrency: Structure versus Automata. LNCS, vol. 1043, pp. 238–266. Springer, Berlin (1996)
Wegener, I.: BDDs design, analysis, complexity, and applications. Discrete Appl. Math. 138, 229–251 (2004)
Woelfel, R.: Symbolic topological sorting with OBDDs. J. Discrete Algorithms (2006, to appear) (also in MFCS’03, LNCS, vol. 2747, pp. 671–680)
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–1230 (2000)
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)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Gentilini, R., Piazza, C. & Policriti, A. Symbolic Graphs: Linear Solutions to Connectivity Related Problems. Algorithmica 50, 120–158 (2008). https://doi.org/10.1007/s00453-007-9079-5
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00453-007-9079-5