Description

Several algorithms exist for the decomposition of strongly-connected-components (SCCs) on a parallel architecture. However, it remains unclear whether these algorithms are well-suited for an on-the-fly implementation (to be able to detect SCCs while constructing the graph - which is useful for several verification techniques). This project will focus on the analysis and design of parallel on-the-fly SCC algorithms. 

For the project, aside from modifying existing parallel algorithms, it is interesting to consider parallelizing depth-first-search (DFS) methods as shown by the recent concurrent version [1] of Tarjan's Algorithm. This suggests that is possible to design an efficient parallel path-based algorithm, in which cycles are contracted during a DFS. The path-based approach is beneficial when dealing with large SCCs in which the on-the-fly property would otherwise suffer [2]. The modified and designed algorithms will be analyzed and compared with each other to find out what is the best parallel on-the-fly SCC decomposition algorithm.

[1] G. Lowe - Concurrent Depth-First Search Algorithms
[2] S. Schwoon and J. Esparza - A Note on On-The-Fly Verification Algorithms

Additional Resources

1. The paper