Sep 25, 2012: Alfons Laarman: Improved Multi-Core Nested Depth-First Search

September 25, 2012Improved Multi-Core Nested Depth-First Search
Room: Zi 5126Alfons Laarman

LTL model checking can be reduced to finding accepting cycles in a graph. While the problem of finding accepting cycles is P-complete and hence likely cannot be parallelized efficiently, several algorithms have shown that in practice good speedups are possible. The OWCTY algorithm was the first to do so. Recently a branch of parallel nested depth-first search (NDFS) is also showing promising results.


I will present the CNDFS algorithm, a tight integration of two earlier multi-core NDFS algorithms for LTL model checking. CNDFS combines the different strengths and avoids some weaknesses of its predecessors:

* it features excellent speedups,

* it is completely on-the-fly,

* it finds shorter counter examples than even a BFS-based algorithm, and

* it uses less memory.