Parallel Reachability Analysis for Hybrid Systems
This work addresses performance bottlenecks in model checking for hybrid systems, offering incremental improvements for multi-core systems.
The authors tackled the problem of inefficient parallel state-space exploration for hybrid systems by proposing two algorithms, with the second achieving better load balancing and a maximum speed-up of 900x on a navigation benchmark compared to SpaceEx LGG scenario.
We propose two parallel state-space exploration algorithms for hybrid systems with the goal of enhancing performance on multi-core shared memory systems. The first is an adaption of the parallel breadth first search in the SPIN model checker. We show that the adapted algorithm does not provide the desired load balancing for many hybrid systems benchmarks. The second is a task parallel algorithm based on cheaply precomputing cost of post (continuous and discrete) operations for effective load balancing. We illustrate the task parallel algorithm and the cost precomputation of post operators on a support-function-based algorithm for state-space exploration. The performance comparison of the two algorithms displays a better CPU utilization/load-balancing of the second over the first, except for certain cases. The algorithms are implemented in the model checker XSpeed and our experiments show a maximum speed-up of $900\times$ on a navigation benchmark with respect to SpaceEx LGG scenario, comparing on the basis of equal number of post operations evaluated.