License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.MEMICS.2010.1
URN: urn:nbn:de:0030-drops-30729
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2011/3072/
Go to the corresponding OASIcs Volume Portal

Bauch, Petr ; Ceska, Milan

CUDA Accelerated LTL Model Checking -­ Revisited

pdf-format:
16.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{bauch_et_al:OASIcs:2011:3072,
  author =	{Petr Bauch and Milan Ceska},
  title =	{{CUDA Accelerated LTL Model Checking -­ Revisited}},
  booktitle =	{Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers},
  pages =	{1--8},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-22-4},
  ISSN =	{2190-6807},
  year =	{2011},
  volume =	{16},
  editor =	{Ludek Matyska and Michal Kozubek and Tom{\'a}{\v{s}} Vojnar and Pavel Zemc{\'i}k and David Antos},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2011/3072},
  URN =		{urn:nbn:de:0030-drops-30729},
  doi =		{10.4230/OASIcs.MEMICS.2010.1},
  annote =	{Keywords: LTL Model Checking, CUDA, OWCTY}
}

Keywords: LTL Model Checking, CUDA, OWCTY
Collection: Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers
Issue Date: 2011
Date of publication: 11.03.2011

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI