Designing Fast LTL Model Checking Algorithms for Many-core GPUs
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F12%3A00057210" target="_blank" >RIV/00216224:14330/12:00057210 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1016/j.jpdc.2011.10.015" target="_blank" >http://dx.doi.org/10.1016/j.jpdc.2011.10.015</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1016/j.jpdc.2011.10.015" target="_blank" >10.1016/j.jpdc.2011.10.015</a>
Alternative languages
Result language
angličtina
Original language name
Designing Fast LTL Model Checking Algorithms for Many-core GPUs
Original language description
Recent technological developments made various many-core hardware platforms widely accessible. These massively parallel architectures have been used to significantly accelerate many computation demanding tasks. In this paper we show how the algorithms for LTL model checking can be redesigned in order to accelerate LTL model checking on many-core GPU platforms. Our detailed experimental evaluation demonstrates that using the NVIDIA CUDA technology results in a significant speedup of the verification process. Together with state space generation based on shared hash-table and DFS exploration, our CUDA accelerated model checker is the fastest among state-of-the-art shared memory model checking tools. The effective utilisation of CUDA technology, however,is quite often reduced by the costly preparation of suitable data structures and limited to small or middle-sized instances due to space limitations, which is also the case of our CUDA-aware LTL Model Checking solutions.
Czech name
—
Czech description
—
Classification
Type
J<sub>x</sub> - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
Result was created during the realization of more than one project. More information in the Projects tab.
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>Z - Vyzkumny zamer (s odkazem do CEZ)<br>S - Specificky vyzkum na vysokych skolach
Others
Publication year
2012
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
Journal of Parallel and Distributed Computing
ISSN
0743-7315
e-ISSN
—
Volume of the periodical
72
Issue of the periodical within the volume
9
Country of publishing house
CZ - CZECH REPUBLIC
Number of pages
15
Pages from-to
1083-1097
UT code for WoS article
000307156000005
EID of the result in the Scopus database
—