"CUDA Accelerated LTL Model Checking - Revisited"@en . . . "P(GA201/09/1389), P(GD102/09/H042)" . "8"^^ . . "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."@en . "2011-01-01+01:00"^^ . "[441913A8AC59]" . "RIV/00216224:14330/11:00049765!RIV12-GA0-14330___" . . . . "CUDA Accelerated LTL Model Checking - Revisited" . "CUDA Accelerated LTL Model Checking - Revisited" . "Sixth Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS'10) -- Selected Papers" . . . "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." . "978-3-939897-22-4" . "\u010Ce\u0161ka, Milan" . "CUDA Accelerated LTL Model Checking - Revisited"@en . . "Dagstuhl, Germany" . . . "Dagstuhl, Germany" . . . . "Linear Temporal Logic (LTL) Model Checking; massively parallel architecture; One Way Catch Them Young (OWCTY) algorithm"@en . . . "2"^^ . "14330" . "Bauch, Petr" . . "2"^^ . . . "192444" . "2190-6807" . "Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik" . "RIV/00216224:14330/11:00049765" .