
arXiv: 1606.05473
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.
16 Pages, LNCS style
Software Engineering (cs.SE), FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Computer Science - Software Engineering, Computer Science - Distributed, Parallel, and Cluster Computing, Distributed, Parallel, and Cluster Computing (cs.DC), Logic in Computer Science (cs.LO)
Software Engineering (cs.SE), FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Computer Science - Software Engineering, Computer Science - Distributed, Parallel, and Cluster Computing, Distributed, Parallel, and Cluster Computing (cs.DC), Logic in Computer Science (cs.LO)
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 6 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
