Parallel reachability analysis for hybrid systems Article Swipe
YOU?
·
· 2016
· Open Access
·
· DOI: https://doi.org/10.1109/memcod.2016.7797741
· OA: W2422398296
We propose two parallel state-space exploration algorithms for hybrid systems\nwith the goal of enhancing performance on multi-core shared memory systems. The\nfirst is an adaption of the parallel breadth first search in the SPIN model\nchecker. We show that the adapted algorithm does not provide the desired load\nbalancing for many hybrid systems benchmarks. The second is a task parallel\nalgorithm based on cheaply precomputing cost of post (continuous and discrete)\noperations for effective load balancing. We illustrate the task parallel\nalgorithm and the cost precomputation of post operators on a\nsupport-function-based algorithm for state-space exploration. The performance\ncomparison of the two algorithms displays a better CPU\nutilization/load-balancing of the second over the first, except for certain\ncases. The algorithms are implemented in the model checker XSpeed and our\nexperiments show a maximum speed-up of $900\\times$ on a navigation benchmark\nwith respect to SpaceEx LGG scenario, comparing on the basis of equal number of\npost operations evaluated.\n