Concurrent Depth-First Search Algorithms

Abstract

We present concurrent algorithms, based on depth-first search, for three problems relevant to model checking: given a state graph, to find its strongly connected components, which states are in loops, and which states are in “lassos”. Our algorithms typically exhibit about a four-fold speed-up over the corresponding sequential algorithms on an eight-core machine. 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.