Parallel state space exploration of linear systems with inputs using XSpeed
Rajarshi Ray, Amit Gurung · 2015
We present on-going work on XSpeed, a tool for parallel state space exploration of continuous systems with linear dynamics and non-deterministic inputs. XSpeed exploits the computational power of multi-core architectures to speed up reachability analysis. A parallel exploration algorithm with multiple initial sets in partitions of the time horizon has been proposed and implemented in XSpeed. A parallel implementation of a reachability algorithm using support functions as symbolic states is also provided. Performance of XSpeed is compared with an optimized implementation of the support function algorithm and with SpaceEx (LGG scenario), a scalable tool for hybrid systems with linear dynamics. Experiments on Intel core i7-4770 having 4 physical cores and 8 threads of execution show that XSpeed achieves a speed up of 5 times when compared to SpaceEx over a 28 dimensional Helicopter model. We could also show computation of precise reachable states with our parallel exploration algorithm in comparison to the support function algorithm.