CUDA Accelerated LTL Model Checking -­ Revisited

Authors Petr Bauch, Milan Ceska



PDF
Thumbnail PDF

File

OASIcs.MEMICS.2010.1.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)
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)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail