×

zbMATH — the first resource for mathematics

Efficient GPU algorithms for parallel decomposition of graphs into strongly connected and maximal end components. (English) Zbl 1404.68204
Summary: This article 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 graphs induced by 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 (as well as existing parallel) counterparts in several case studies.

MSC:
68W10 Parallel algorithms in computer science
05C40 Connectivity
05C85 Graph algorithms (graph-theoretic aspects)
68Q60 Specification and verification (program logics, model checking, etc.)
68R10 Graph theory (including graph drawing) in computer science
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Barnat J, Bauch P, Brim L, Ceska M (2011) Computing Strongly Connected Components in Parallel on CUDA. In: IPDPS, IEEE, pp 544-555
[2] de Alfaro L (1998) How to specify and verify the long-run average behavior of probabilistic systems. In: LICS, IEEE Computer Society, pp 454-465
[3] Stuhl M (2013) Computing Strongly Connected Components with CUDA. Master’s thesis, Masaryk University
[4] Ábrahám E, Jansen N, Wimmer R, Katoen JP, Becker B (2010) DTMC model checking by SCC reduction. In: QEST, IEEE Computer Society, pp 37-46 · Zbl 1238.91025
[5] Baier C, Katoen JP (2008) Principles of model checking. the mit press, Cambridge · Zbl 1179.68076
[6] Barnat J, Brim L, Ceska M, Lamr T (2009) CUDA accelerated LTL model checking. In: ICPADS, IEEE, pp 34-41 · Zbl 1082.68086
[7] Barnat, J; Moravec, P, Parallel algorithms for finding SCCs in implicitly given graphs, FMICS/PDMC, 4346, 316-330, (2007)
[8] Bloem, R; Gabow, H; Somenzi, F, An algorithm for strongly connected component analysis in \( \)\(n {\rm log} n\)\( \) symbolic steps, Formal Method Syst Design, 28, 37-56, (2006) · Zbl 1110.68161
[9] Bloem, R; Gabow, HN; Somenzi, F, An algorithm for strongly connected component analysis in \( \)\(n \log n\)\( \) symbolic steps, Formal Method Syst Design, 28, 37-56, (2006) · Zbl 1110.68161
[10] Bošnački, D; Edelkamp, S; Sulewski, D; Wijs, A, Parallel probabilistic model checking on general purpose graphic processors, STTT, 13, 21-35, (2011)
[11] Bošnački D, Edelkamp S, Sulewski D, Wijs A (2010) GPU-PRISM: An extension of PRISM for general purpose graphics processing units. In: PDMC 2010, IEEE, pp 17-19 · Zbl 1295.91019
[12] Bruyère, V; Filiot, E; Randour, M; Raskin, JF, Meet your expectations with guarantees: beyond worst-case synthesis in quantitative games, STACS, Schloss Dagstuhl, LIPIcs, 25, 199-213, (2014) · Zbl 1360.91042
[13] Chatterjee K, Henzinger M (2011) Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification. In: SODA, SIAM, pp 1318-1336 · Zbl 1374.68272
[14] Chatterjee K, Henzinger M (2012) An \( \)\(O(n^2)\)\( \) time algorithm for alternating büchi games. In: SODA, SIAM, pp 1386-1399
[15] Chatterjee, K; Henzinger, M, Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition, J ACM, 61, 15, (2014) · Zbl 1295.91019
[16] Chatterjee, K; Łącki, J, Faster algorithms for Markov decision processes with low treewidth, CAV, 8044, 543-558, (2013)
[17] Courcoubetis, C; Yannakakis, M, The complexity of probabilistic verification, J ACM, 42, 857-907, (1995) · Zbl 0885.68109
[18] Dijkstra EW, Feijen WHJ (1988) A method of programming. Addison-Wesley, Boston · Zbl 0681.68001
[19] Edelkamp S, Sulewski D (2010) Efficient Explicit-state model checking on general purpose graphics processors. SPIN, Springer, LNCS 6349:106-123 · Zbl 1110.68161
[20] Fleischer L, Hendrickson B, Pinar A (2000) On identifying strongly connected components in parallel. In: IPDPS workshop irregular 2000, Springer, LNCS, vol 1800, pp 505-511, http://dl.acm.org/citation.cfm?id=645612.663154
[21] Gentilini R, Piazza C, Policriti A (2003) Computing strongly connected components in a linear number of symbolic steps. In: SODA, ACM/SIAM, pp 573-582 · Zbl 1092.68716
[22] Harish P, Narayanan P (2007) Accelerating Large Graph Algorithms on the GPU Using CUDA. HiPC, Springer, Heidelberg, 4873:197-208 · Zbl 0885.68109
[23] Hong S, Rodia N, Olukotun K (2013) On fast parallel detection of strongly connected components (SCC) in Small-World Graphs. In: SC’13, ACM, p 92
[24] Kwiatkowska MZ, Parker D, Qu H, Ujma M (2014) On incremental quantitative verification for probabilistic systems. In: Voronkov A, Korovina MV (eds) HOWARD-60: A Festschrift on the Occasion of Howard Barringer’s 60th Birthday, EasyChair, pp 245-257
[25] Kwiatkowska M, Norman G, Parker D (2011) PRISM 4.0: Verification of probabilistic real-time systems. In: CAV, Springer, LNCS, vol 6806, pp 585-591
[26] Li, G; Zhu, Z; Cong, Z; Yang, F, Efficient decomposition of strongly connected components on gpus, J Syst Architect, 60, 1-10, (2014)
[27] McLendon, W; Hendrickson, B; Plimpton, S; Rauchwerger, L, Finding strongly connected components in distributed graphs, J Parallel Distrib Comput, 65, 901-910, (2005) · Zbl 1082.68086
[28] Merrill D, Garland M, Grimshaw A (2012) Scalable GPU graph traversal. In: PPoPP, ACM, pp 117-128
[29] Orzan S (2004) On distributed verification and verified distribution. PhD thesis, Free University of Amsterdam · Zbl 1238.91025
[30] Tarjan, R, Depth-first search and linear graph algorithms, SIAM J Comput, 1, 146-160, (1972) · Zbl 0251.05107
[31] Ummels, M; Wojtczak, D, The complexity of Nash equilibria in stochastic multiplayer games, Logical Method Comput Sci, 7, 1-45, (2011) · Zbl 1238.91025
[32] Wang, C; Bloem, R; Hachtel, GD; Ravi, K; Somenzi, F, Compositional SCC analysis for language emptiness, Formal Method Syst Design, 28, 5-36, (2006) · Zbl 1100.68059
[33] Wijs A (2015) GPU accelerated strong and branching bisimilarity checking. In: TACAS’15, Springer, LNCS, vol 9035, pp 368-383
[34] Wijs A, Bošnački D (2012) Improving GPU sparse matrix-vector multiplication for probabilistic model checking. SPIN, Springer, LNCS 7385:98-116
[35] Wijs A, Bošnački D (2014) GPUexplore: many-core on-the-fly state space exploration. TACAS, Springer, LNCS 8413:233-247
[36] Wijs A, Katoen JP, Bošnački D (2014) GPU-based graph decomposition into strongly connected and maximal end components. CAV, Springer, LNCS 8559:309-325
[37] Xie A, Beerel P (1999) Implicit enumeration of strongly connected components. In: CAD’99, pp 37-40
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.