The report FIMU-RS-2009-05
CUDA accelerated LTL Model Checking
June 2009, 18 pages.
Available as Postscript,
Recent technological developments made available various many-core hardware platforms. For example,
a SIMD-like hardware architecture became easily accessible for many users who have their computers
equipped with modern NVIDIA GPU cards with CUDA technology. In this paper we redesign the
maximal accepting predecessors algorithm  for LTL model checking in terms of matrix-vector product
in order to accelerate LTL model checking on many-core GPU platforms. Our experiments demonstrate
that using the NVIDIA CUDA technology results in a significant computation speedup.