Computer Science – Distributed – Parallel – and Cluster Computing
Scientific paper
2009-12-14
EPTCS 14, 2009, pp. 107-111
Computer Science
Distributed, Parallel, and Cluster Computing
Scientific paper
10.4204/EPTCS.14.8
In this paper we present a tool that performs CUDA accelerated LTL Model Checking. The tool exploits parallel algorithm MAP adjusted to the NVIDIA CUDA architecture in order to efficiently detect the presence of accepting cycles in a directed graph. Accepting cycle detection is the core algorithmic procedure in automata-based LTL Model Checking. We demonstrate that the tool outperforms non-accelerated version of the algorithm and we discuss where the limits of the tool are and what we intend to do in the future to avoid them.
Barnat Jiří
Brim Luboš
Češka Milan
No associations
LandOfFree
DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and DiVinE-CUDA - A Tool for GPU Accelerated LTL Model Checking will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-623960