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

Event Details

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.

This is joint work with Muhammad Osama