Parallel Reachability Analysis for Hybrid Systems

TL;DR

This paper introduces two parallel algorithms for hybrid systems' state-space exploration, improving performance and load balancing on multi-core systems, with the second algorithm showing superior CPU utilization and significant speed-up.

Contribution

It presents a novel task parallel algorithm with cost precomputation for hybrid systems, outperforming a parallel BFS adaptation in load balancing and efficiency.

Findings

Second algorithm achieves better load balancing than the first.

Maximum speed-up of 900x on a navigation benchmark.

Implementation in XSpeed demonstrates significant performance gains.

Abstract

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.