Sep 20, 2011: Jaco van de Pol: Parallel Nested Depth First Search

September 20, 2011Parallel Nested Depth First Search
Room: Zi 5126Jaco van de Pol

The LTL Model Checking problem is reducible to finding accepting cycles in a graph. The Nested Depth-First Search (NDFS) algorithm detects accepting cycles efficiently: on-the-fly, with linear-time complexity and negligible memory overhead.

The only downside of the algorithm is that it relies on depth-first search, which is inherently sequential. It has not been parallelized beyond running the independent nested search in a separate thread (dual core).

We will present a multi-core NDFS-algorithm that can scale beyond two threads, while maintaining linear-time worst-case complexity. We prove this algorithm correct, and present experimental results obtained with an implementation in the LTSmin tool set on the entire BEEM benchmark database.  We measured considerable speedups compared to the current state of the art in parallel cycle detection algorithms.