GPU-Based Graph Decomposition into Strongly Connected and Maximal End Components

  • Anton Wijs
  • Joost-Pieter Katoen
  • Dragan Bošnački
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8559)


This paper presents parallel algorithms for component decomposition of graph structures on General Purpose Graphics Processing Units (GPUs). In particular, we consider the problem of decomposing sparse graphs into strongly connected components, and decomposing stochastic games (such as Markov decision processes) into maximal end components. These problems are key ingredients of many (probabilistic) model-checking algorithms. We explain the main rationales behind our GPU-algorithms, and show a significant speed-up over the sequential counterparts in several case studies.


Model Check Central Processing Unit Markov Decision Process Global Memory Stochastic Game 
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.


  1. 1.
    Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press (2008)Google Scholar
  2. 2.
    Wang, C., Bloem, R., Hachtel, G.D., Ravi, K., Somenzi, F.: Compositional SCC analysis for language emptiness. Formal Methods in System Design 28, 5–36 (2006)CrossRefzbMATHGoogle Scholar
  3. 3.
    Tarjan, R.E.: Depth-First Search and Linear Graph Algorithms. SIAM J. Comput. 1(2), 146–160 (1972)CrossRefzbMATHMathSciNetGoogle Scholar
  4. 4.
    Bloem, R., Gabow, H.N., Somenzi, F.: An Algorithm for Strongly Connected Component Analysis in n log n Symbolic Steps. Formal Methods in System Design 28, 37–56 (2006)CrossRefzbMATHGoogle Scholar
  5. 5.
    Barnat, J., Bauch, P., Brim, L., Ceska, M.: Computing Strongly Connected Components in Parallel on CUDA. In: IPDPS, pp. 544–555. IEEE (2011)Google Scholar
  6. 6.
    Hong, S., Rodia, N., Olukotun, K.: On Fast Parallel Detection of Strongly Connected Components (SCC) in Small-World Graphs. In: SC 2013, p. 92. ACM (2013)Google Scholar
  7. 7.
    Li, G., Zhu, Z., Cong, Z., Yang, F.: Efficient Decomposition of Strongly Connected Components on GPUs. Journal of Systems Architecture 60(1), 1–10 (2014)CrossRefGoogle Scholar
  8. 8.
    Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857–907 (1995)CrossRefzbMATHMathSciNetGoogle Scholar
  9. 9.
    de Alfaro, L.: How to specify and verify the long-run average behavior of probabilistic systems. In: LICS, 454–465. IEEE Computer Society (1998)Google Scholar
  10. 10.
    Ummels, M., Wojtczak, D.: The Complexity of Nash Equilibria in Stochastic Multiplayer Games. Logical Methods in Computer Science 7 (2011)Google Scholar
  11. 11.
    Bruyère, V., Filiot, E., Randour, M., Raskin, J.-F.: Meet your expectations with guarantees: Beyond worst-case synthesis in quantitative games. In: STACS. LIPIcs, vol. 25, pp. 199–213. Schloss Dagstuhl (2014)Google Scholar
  12. 12.
    Chatterjee, K., Henzinger, M.: Faster and Dynamic Algorithms for Maximal End-Component Decomposition and Related Graph Problems in Probabilistic Verification. In: SODA, pp. 1318–1336. SIAM (2011)Google Scholar
  13. 13.
    Chatterjee, K., Łącki, J.: Faster Algorithms for Markov Decision Processes with Low Treewidth. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 543–558. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  14. 14.
    Fleischer, L.K., Hendrickson, B.A., Pinar, A.: On identifying strongly connected components in parallel. In: Rolim, J.D.P. (ed.) IPDPS-WS 2000. LNCS, vol. 1800, pp. 505–511. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  15. 15.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of Probabilistic Real-time Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  16. 16.
    Bošnački, D., Edelkamp, S., Sulewski, D., Wijs, A.J.: Parallel Probabilistic Model Checking on General Purpose Graphic Processors. STTT 13(1), 21–35 (2011)CrossRefGoogle Scholar
  17. 17.
    Barnat, J., Brim, L., Ceska, M., Lamr, T.: CUDA Accelerated LTL Model Checking. In: ICPADS, 34–41. IEEE (2009)Google Scholar
  18. 18.
    Edelkamp, S., Sulewski, D.: Efficient Explicit-State Model Checking on General Purpose Graphics Processors. In: van de Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol. 6349, pp. 106–123. Springer, Heidelberg (2010)Google Scholar
  19. 19.
    Wijs, A.J., Bošnački, D.: Improving GPU Sparse Matrix-Vector Multiplication for Probabilistic Model Checking. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 98–116. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  20. 20.
    Bošnački, D., Edelkamp, S., Sulewski, D., Wijs, A.: GPU-PRISM: An Extension of PRISM for General Purpose Graphics Processing Units. In: PDMC 2010, pp. 17–19. IEEE (2010)Google Scholar
  21. 21.
    Wijs, A., Bošnački, D.: GPUexplore: Many-Core On-The-Fly State Space Exploration. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 233–247. Springer, Heidelberg (2014)Google Scholar
  22. 22.
    Chatterjee, K., Henzinger, M.: An O(n 2) Time Algorithm for Alternating Büchi Games. In: SODA, pp. 1386–1399. SIAM (2012)Google Scholar
  23. 23.
    Dijkstra, E.W., Feijen, W.H.J.: A Method of Programming. Addison-Wesley (1988)Google Scholar
  24. 24.
    McLendon III, W., Hendrickson, B., Plimpton, S., Rauchwerger, L.: Finding Strongly Connected Components in Distributed Graphs. J. Parallel Distrib. Comput. 65, 901–910 (2005)CrossRefzbMATHGoogle Scholar
  25. 25.
    Orzan, S.: On Distributed Verification and Verified Distribution. PhD thesis, Free University of Amsterdam (2004)Google Scholar
  26. 26.
    Barnat, J., Moravec, P.: Parallel Algorithms for Finding SCCs in Implicitly Given Graphs. In: Brim, L., Haverkort, B.R., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol. 4346, pp. 316–330. Springer, Heidelberg (2007)Google Scholar
  27. 27.
    Harish, P., Narayanan, P.J.: Accelerating Large Graph Algorithms on the GPU Using CUDA. In: Aluru, S., Parashar, M., Badrinath, R., Prasanna, V.K. (eds.) HiPC 2007. LNCS, vol. 4873, pp. 197–208. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  28. 28.
    Merrill, D., Garland, M., Grimshaw, A.: Scalable GPU Graph Traversal. In: PPoPP, 117–128. ACM (2012)Google Scholar
  29. 29.
    Stuhl, M.: Computing Strongly Connected Components with CUDA. Master’s thesis, Masaryk University (2013)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Anton Wijs
    • 1
  • Joost-Pieter Katoen
    • 2
  • Dragan Bošnački
    • 1
  1. 1.Eindhoven University of TechnologyThe Netherlands
  2. 2.RWTH Aachen UniversityGermany

Personalised recommendations