Multi-core nested depth-first search. (English) Zbl 1348.68142

Bultan, Tevfik (ed.) et al., Automated technology for verification and analysis. 9th international symposium, ATVA 2011, Taipei, Taiwan, October 11–14, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-24371-4/pbk). Lecture Notes in Computer Science 6996, 321-335 (2011).
Summary: 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 an inherently-sequential, depth-first search. It has not been parallelized beyond running the independent nested search in a separate thread (dual core).
In this paper, we introduce, for the first time, a multi-core NDFS algorithm that can scale beyond two threads, while maintaining exactly the same worst-case time 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.
For the entire collection see [Zbl 1223.68004].


68Q60 Specification and verification (program logics, model checking, etc.)
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68W10 Parallel algorithms in computer science


DiVinE; LTSmin
Full Text: DOI