CUDA Accelerated LTL Model Checking - Revisited

• Authors: BAUCH Petr; ČEŠKA Milan
• Year of publication: 2011
• Type: Article in Proceedings
• Conference: Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers
• MU Faculty or unit: Faculty of Informatics
• Web: http://drops.dagstuhl.de/opus/volltexte/2011/3072
• Field: Informatics
• Keywords: Linear Temporal Logic (LTL) Model Checking; massively parallel architecture; One Way Catch Them Young (OWCTY) algorithm
• Description: 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.

Related projects

• Verification and Analysis of Large-Scale Computer Systems
• 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