Algorithms for SCC Decomposition

We study and improve the OBF technique [Barnat, J. and P.Moravec, Parallel algorithms for finding SCCs in implicitly given graphs, in: Proceedings of the 5th International Workshop on Parallel and Distributed Methods in Verification (PDMC 2006), LNCS (2007)], which was used in distributed algorithms for the decomposition of a partitioned graph into its strongly connected components. In particular, we introduce a recursive variant of OBF and experimentally evaluate several different implementations of it that vary in the degree of parallelism. For the evaluation we used synthetic graphs with a few large components and graphs with many small components. We also experimented with graphs that arise as state spaces in real model checking applications. The experimental results are compared with that of other successful SCC decomposition techniques [Orzan, S., ''On Distributed Verification and Verified Distribution,'' Ph.D. thesis, Free University of Amsterdam (2004); Fleischer, L.K., B. Hendrickson and A. Pinar, On identifying strongly connected components in parallel, in: Parallel and Distributed Processing, IPDPS Workshops, Lecture Notes in Computer Science 1800, 2000, pp. 505-511].