10.4230/OASICS.MEMICS.2010.1
Bauch, Petr
Petr
Bauch
Ceska, Milan
Milan
Ceska
CUDA Accelerated LTL Model Checking - Revisited
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
2011
Article
LTL Model Checking
CUDA
OWCTY
Matyska, Ludek
Ludek
Matyska
Kozubek, Michal
Michal
Kozubek
Vojnar, Tomáš
Tomáš
Vojnar
Zemcík, Pavel
Pavel
Zemcík
Antos, David
David
Antos
2011
2011-03-11
2011-03-11
2011-03-11
en
urn:nbn:de:0030-drops-30729
10.4230/OASIcs.MEMICS.2010
978-3-939897-22-4
2190-6807
10.4230/OASIcs.MEMICS.2010
OASIcs, Volume 16, MEMICS 2010
Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers
2012
16
1
1
8
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Matyska, Ludek
Ludek
Matyska
Kozubek, Michal
Michal
Kozubek
Vojnar, Tomáš
Tomáš
Vojnar
Zemcík, Pavel
Pavel
Zemcík
Antos, David
David
Antos
2190-6807
Open Access Series in Informatics (OASIcs)
2011
16
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
8 pages
486279 bytes
application/pdf
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
info:eu-repo/semantics/openAccess
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.
OASIcs, Vol. 16, Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers, pages 1-8