CUDA Accelerated LTL Model Checking - Revisited

Varování

Publikace nespadá pod Ústav výpočetní techniky, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Autoři	BAUCH Petr ČEŠKA Milan
Rok publikování	2011
Druh	Článek ve sborníku
Konference	Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
www	http://drops.dagstuhl.de/opus/volltexte/2011/3072
Obor	Informatika
Klíčová slova	Linear Temporal Logic (LTL) Model Checking; massively parallel architecture; One Way Catch Them Young (OWCTY) algorithm
Popis	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.
Související projekty:	Verifikace a analýza velmi velkých počítačových systémů Matematické a inženýrské metody pro vývoj spolehlivých a bezpečných paralelních a distribuovaných počítačových systémů Rozsáhlé výpočetní systémy: modely, aplikace a verifikace