GPUexplore 3.0: GPU Accelerated State Space Exploration for Concurrent Systems with Data

GPUexplore 3.0 is an explicit state space exploration tool that runs entirely on a graphics processing unit (GPU), and supports models of concurrent systems with data variables. We discuss its workflow and modelling language, present several design decisions regarding work distribution and retrieval, and experimentally evaluate the impact of those decisions. Our tool achieves acceleration up to 115 $$\times $$ and 28 $$\times $$ compared to single- and four-core LTSmin, respectively. It currently checks for deadlocks, with verification of temporal logic formulae planned for the near future.