Multi-core nested-depth first search

A. Laarman, R. Langerak, J.C. Pol, van de, M. Weber, A.J. Wijs

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

28 Citations (Scopus)
4 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationProceedings of the 9th International Symposium on Automated Technology for Verification and Analysis
EditorsT. Bultan, P.-A. Hsiung
Place of PublicationHeidelberg
PublisherSpringer
Pages321-335
ISBN (Print)978-3-642-24372-1
DOIs
Publication statusPublished - 2011

Publication series

NameLecture Notes in Computer Science
Volume6996
ISSN (Print)0302-9743

Fingerprint

Dive into the research topics of 'Multi-core nested-depth first search'. Together they form a unique fingerprint.

Cite this