Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
Multi-core Nested Depth-First Search
verfasst von : Alfons Laarman, Rom Langerak, Jaco van de Pol, Michael Weber, Anton Wijs
Erschienen in: Automated Technology for Verification and Analysis
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.