Paper Info
Title
Multi-core nested depth-first search
Abstract
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.
Year
DOI
Venue
2011
10.1007/978-3-642-24372-1_23
European Journal of Gynaecological Oncology
Keywords
Field
DocType
worst-case time complexity,depth-first search,nested depth-first search,linear-time complexity,ltsmin tool,parallel cycle detection algorithm,independent nested search,algorithm detects,multi-core ndfs algorithm,ltl model checking problem
Graph,Model checking,Computer science,Breadth-first search,Algorithm,Cycle detection,Thread (computing),Linear temporal logic,Time complexity,Multi-core processor
Conference
Volume
ISSN
Citations 
6996
0302-9743
22
PageRank 
References 
Authors
0.83
17
5
Name
Order
Citations
PageRank
alfons laarman126614.17
Rom Langerak230839.16
Jaco Van De Pol3102278.19
Michael Weber424011.93
Anton Wijs520322.84