Parallel Nested Depth-First Searches for LTL Model Checking

Even though the well-known nested-depth first search algorithm for LTL model checking provides good performance, it cannot benefit from the recent advent of multi-core computers. This paper proposes a new version of this algorithm, adapted to multi-core architectures with a shared memory. It can exhibit good speed-ups as supported by a series of experiments.

• Type: Journal
• Year: 2011
• Where: ATVA
• Authors: Sami Evangelista, Laure Petrucci, Samir Youcef
• Keywords: ATVA 2011, Hardware, Search Algorithm, Shared Memory, Speed Ups