GPUexplore, a GPU-accelerated explicit-state LTL model checker, achieves significant speedups compared to sequential and multi-core CPU model checkers, but it is limited by the amount of memory available on GPUs. Partial-Order Reduction is a way to remedy this problem, by excluding unnecessary transitions and states from exploration. For this work, we implemented the ample and clustered-ample reduction techniques in GPUexplore. Experiments show that our implementations achieve reductions similar to the state-of-the-art Breadth-First Search configurations of multi-core LTSmin and sequential DiVinE and Spin without introducing significant computational overhead, even though LTSmin applies stubborn set reduction, which has often been reported as the most effective technique. At times, ample and cample reduction even speeds up exploration 4-100×.

This is joint work with Rik van Spreuwel