CUDA Accelerated LTL Model Checking -­ Revisited

Authors Petr Bauch, Milan Ceska

Thumbnail PDF


  • Filesize: 474 kB
  • 8 pages

Document Identifiers

Author Details

Petr Bauch
Milan Ceska

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)


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.
  • LTL Model Checking
  • CUDA


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads