The need for massively parallel algorithms, suitable to exploit the computational power of hardware such as graphics processing units, is ever increasing. We propose a new explicit-state model checking algorithm for the on-the-fly verification of Linear-Time Temporal Logic (LTL) formulae that is aimed at running on such devices. We prove its correctness and termination guarantee, and experimentally compare a GPU implementation within the GPUexplore model checker with state-of-the-art CPU-based LTL model checkers. Our new algorithm is up to 150 times faster on proving the correctness of a system than the LTSmin tool running on a 32-core high-end CPU, and is more economic in using the available memory.
Program Display Configuration
Tue 16 Apr
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Viennachange