OASIcs.MEMICS.2010.1.pdf
- Filesize: 474 kB
- 8 pages
Document
CUDA Accelerated LTL Model Checking - Revisited
Authors
-
Part of:
Volume:
Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers (MEMICS 2010)
Series: Open Access Series in Informatics (OASIcs) - License:
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
- Publication Date: 2011-03-11
Cite AsGet BibTex
Petr Bauch and Milan Ceska. CUDA Accelerated LTL Model Checking - Revisited. In Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers. Open Access Series in Informatics (OASIcs), Volume 16, pp. 1-8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)
https://doi.org/10.4230/OASIcs.MEMICS.2010.1
https://doi.org/10.4230/OASIcs.MEMICS.2010.1
Abstract
Recently, the massively parallel architecture has been used to significantly accelerate many computation demanding tasks. For example, in [Baier, Kateon, The MIT Press, 2009; Barnat, Brim, Ceska, ICPADS 2009] we have shown how CUDA technology can be employed to accelerate the process of Linear Temporal Logic (LTL) Model Checking. In this paper we redesign the One-Way-Catch-Them-Young (OWCTY) algorithm [Cerna, Pelanek, SPIN'03] in order to devise a new CUDA accelerated OWCTY algorithm that will significantly outperform the original CUDA accelerated algorithm and will be resistant to slowdown caused by improper ordering of the input data representation.
Keywords
- LTL Model Checking
- CUDA
- OWCTY
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads