Hitching a Ride to a Lasso: Massively Parallel On-The-Fly LTL Model Checking

The need for massively parallel algorithms, suitable to exploit the computational power of hardware such as graphics processing units, is ever increasing. In this paper, we propose a new algorithm for the on-the-fly verification of Linear-Time Temporal Logic (LTL) formulae [45] that is aimed at running on such devices. We prove its correctness and termination guarantee, and experimentally compare a GPU implementation with state-of-the-art LTL model checkers. Our new GPU LTL-checking algorithm is up to 150 \(\times \) faster on proving the correctness of a system than LTSmin running on a 32-core high-end CPU, and is more economic in using the available memory.