CUDA Accelerated LTL Model Checking - Revisited
| Authors | |
|---|---|
| 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 | |
| Citation | |
| 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: |