Advertisement

An Algorithm for Strongly Connected Component Analysis in n log n Symbolic Steps

  • Roderick Bloem
  • Harold N. Gabow
  • Fabio Somenzi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1954)

Abstract

We present a symbolic algorithm for strongly connected component decomposition. The algorithm performs Θ(n log n) image and preimage computations in the worst case, where n is the number of nodes in the graph. This is an improvement over the previously known quadratic bound. The algorithm can be used to decide emptiness of Büchi automata with the same complexity bound, improving Emerson and Lei’ quadratic bound, and emptiness of Streett automata, with a similar bound in terms of nodes. It also leads to an improved procedure for the generation of nonemptiness witnesses.

Keywords

Model Check Transition Relation Transitive Closure Acceptance Condition Strongly Connect Component 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [B+96]
    R. K. Brayton et al. VIS. In Formal Methods in Computer Aided Design, pages 248–256. Springer-Verlag, Berlin, November 1996. LNCS 1166.CrossRefGoogle Scholar
  2. [BRS99]
    R. Bloem, K. Ravi, and F. Somenzi. Efficient decision procedures for model checking of linear time logic properties. In N. Halbwachs and D. Peled, editors, Eleventh Conference on Computer Aided Verification (CAV’99), pages 222–235. Springer-Verlag, Berlin, 1999. LNCS 1633.Google Scholar
  3. [Bry86]
    R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, August 1986.CrossRefGoogle Scholar
  4. [Büc62]
    J. R. Büchi. On a decision method in restricted second order arithmetic. In Proceedings of the 1960 International Congress on Logic, Methodology, and Philosophy of Science, pages 1–11. Stanford University Press, 1962.Google Scholar
  5. [CES86]
    E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications. ACM Transaction on Programming Languages and Systems, 8(2):244–263, 1986.zbMATHCrossRefGoogle Scholar
  6. [CGMZ95]
    E. Clarke, O. Grumberg, K. McMillan, and X. Zhao. Efficient generation of counterexamples and witnesses in symbolic model checking. In Proceedings of the Design Automation Conference, pages 427–432, San Francisco, CA, June 1995.Google Scholar
  7. [CGP99]
    E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, Cambridge, MA, 1999.Google Scholar
  8. [EL86]
    E. A. Emerson and C.-L. Lei. Efficient model checking in fragments of the propositional mu-calculus. In Proceedings of the First Annual Symposium of Logic in Computer Science, pages 267–278, June 1986.Google Scholar
  9. [EL87]
    E. A. Emerson and C. Lei. Modalities for model checking: Branching time logic strikes back. Science of Computer Programming, 8:275–306, 1987.zbMATHCrossRefMathSciNetGoogle Scholar
  10. [ES81]
    S. Even and Y. Shiloach. An on-line edge-deletion problem. Journal of the Association for Computing Machinery, 28(1):1–4, January 1981.zbMATHMathSciNetGoogle Scholar
  11. [HHK96]
    R. H. Hardin, Z. Har’El, and R. P. Kurshan. COSPAN. In Eighth Conference on Computer Aided Verification (CAV’ 96), pages 423–427. Springer-Verlag, 1996. Lncs 1102.Google Scholar
  12. [HKSV97]
    R. H. Hardin, R. P. Kurshan, S. K. Shukla, and M. Y. Vardi. A new heuristic for bad cycle detection using BDDs. In O. Grumberg, editor, Ninth Conference on Computer Aided Verification (CAV’97), pages 268–278. Springer-Verlag, Berlin, 1997. LNCS 1254.Google Scholar
  13. [HLP52]
    G. H. Hardy, J. E. Littlewood, and G. Pólya. Inequalities. Cambridge University Press, 1952.Google Scholar
  14. [HSBK93] R. Hojati, T. R. Shiple, R. Brayton, and R. Kurshan. A unified approach to language containment and fair CTL model checking. In Proceedings of the Design Automation Conference, pages 475–481, June 1993.Google Scholar
  15. [HT96]
    M. R. Henzinger and J. A. Telle. Faster algorithms for the nonemptiness of Streett automata and for communication protocol pruning. In R. Karlsson and A. Lingas, editors, Algorithm Theory: SWAT’96, pages 16–27. Springer-Verlag, Berlin, 1996. LNCS 1097.Google Scholar
  16. [HTKB92]
    R. Hojati, H. Touati, R. P. Kurshan, and R. K. Brayton. Efficient ω-regular language containment. In Computer Aided Verification, pages 371–382, Montréal, Canada, June 1992.Google Scholar
  17. [KPR98]
    Y. Kesten, A. Pnueli, and L.-o. Raviv. Algorithmic verification of linear temporal logic specifications. In International Colloquium on Automata, Languages, and Programming (ICALP-98), pages 1–16, Berlin, 1998. Springer. LNCS 1443.Google Scholar
  18. [Kur94]
    R. P. Kurshan. Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton, NJ, 1994.Google Scholar
  19. [McM87]
    K. McMillan. Class project on BDD-based verification. Private Communication, E. M. Clarke, 1987.Google Scholar
  20. [McM94]
    K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA, 1994.Google Scholar
  21. [McM99]
    K. L. McMillan. Verification of infinite state systems by compositional model checking. In Correct Hardware Design and Verification Methods (CHARME’99), pages 219–233, Berlin, September 1999. Springer-Verlag. LNCS 1703.Google Scholar
  22. [RBS]
    K. Ravi, R. Bloem, and F. Somenzi. A comparative study of symbolic algorithms for the computation of fair cycles. In these proceedings.Google Scholar
  23. [RS97]
    G. Rozenberg and A. Salomaa, editors. Handbook of Formal Languages. Springer, Berlin, 1997.zbMATHGoogle Scholar
  24. [Str82]
    R. S. Streett. Propositional dynamic logic of looping and converse is elementarily decidable. Information and Control, 54:121–141, 1982.zbMATHCrossRefMathSciNetGoogle Scholar
  25. [Tar72]
    R. Tarjan. Depth first search and linear graph algorithms. SIAM Journal of Computing, 1:146–160, 1972.zbMATHCrossRefMathSciNetGoogle Scholar
  26. [TBK95]
    H. J. Touati, R. K. Brayton, and R. P. Kurshan. Testing language containment for ω-automata using BDD’s. Information and Computation, 118(1):101–109, April 1995.zbMATHCrossRefMathSciNetGoogle Scholar
  27. [Tho97]
    W. Thomas. Languages, automata, and logic. In Rozenberg and Salomaa [RS97], chapter 7, Vol. 3, pages 389–455.Google Scholar
  28. [XB99]
    A. Xie and P. A. Beerel. Implicit enumeration of strongly connected components. In Proceedings of the International Conference on Computer-Aided Design, pages 37–40, San Jose, CA, November 1999.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Roderick Bloem
    • 1
  • Harold N. Gabow
    • 1
  • Fabio Somenzi
    • 1
  1. 1.University of Colorado at BoulderUSA

Personalised recommendations