CUDA Accelerated LTL Model Checking

Investor logo
Investor logo
Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BARNAT Jiří BRIM Luboš ČEŠKA Milan LAMR Tomáš

Year of publication 2009
Type Article in Proceedings
Conference Proceedings of the 15th International Conference on Parallel and Distributed Systems
MU Faculty or unit

Faculty of Informatics

Citation
Field Informatics
Keywords Model Checking; Linear Temporal Logic; CUDA
Description 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 [7] 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 speedup of verification process.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.