and Maximal End Components Contractual Date of Delivery to the CEC: 30-Sep-2014 Actual Date of Delivery to the CEC: 31-Ago-2014

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. Note: This deliverable is based on material that has been published in A. Biere and R. Bloem (Eds.): CAV 2014, LNCS 8559