CUDA Accelerated LTL Model Checking - Revisited

• 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
• 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