conference paper published yes Rajarshi Ray author Amit Gurung author Binayak Das author Ezio Bartocci author Sergiy Bogomolov author 369D9A44-F248-11E8-B48F-1D18A9856A870000-0002-0686-0365 Radu Grosu author ToHe department HVC: Haifa Verification Conference Quantitative Reactive Modeling project Moderne Concurrency Paradigms project Rigorous Systems Engineering project Formal methods for the design and analysis of complex systems project We present XSpeed a parallel state-space exploration algorithm for continuous systems with linear dynamics and nondeterministic inputs. The motivation of having parallel algorithms is to exploit the computational power of multi-core processors to speed-up performance. The parallelization is achieved on two fronts. First, we propose a parallel implementation of the support function algorithm by sampling functions in parallel. Second, we propose a parallel state-space exploration by slicing the time horizon and computing the reachable states in the time slices in parallel. The second method can be however applied only to a class of linear systems with invertible dynamics and fixed input. A GP-GPU implementation is also presented following a lazy evaluation strategy on support functions. The parallel algorithms are implemented in the tool XSpeed. We evaluated the performance on two benchmarks including an 28 dimension Helicopter model. Comparison with the sequential counterpart shows a maximum speed-up of almost 7× on a 6 core, 12 thread Intel Xeon CPU E5-2420 processor. Our GP-GPU implementation shows a maximum speed-up of 12× over the sequential implementation and 53× over SpaceEx (LGG scenario), the state of the art tool for reachability analysis of linear hybrid systems. Experiments illustrate that our parallel algorithm with time slicing not only speeds-up performance but also improves precision. Springer2015Haifa, Israel eng 10.1007/978-3-319-26287-1_1 94343 - 18 Ray R, Gurung A, Das B, Bartocci E, Bogomolov S, Grosu R. 2015. XSpeed: Accelerating reachability analysis on multi-core processors. 9434, 3–18. Ray, Rajarshi, Amit Gurung, Binayak Das, Ezio Bartocci, Sergiy Bogomolov, and Radu Grosu. “XSpeed: Accelerating Reachability Analysis on Multi-Core Processors.” Lecture Notes in Computer Science. Springer, 2015. <a href="https://doi.org/10.1007/978-3-319-26287-1_1">https://doi.org/10.1007/978-3-319-26287-1_1</a>. R. Ray, A. Gurung, B. Das, E. Bartocci, S. Bogomolov, and R. Grosu, “XSpeed: Accelerating reachability analysis on multi-core processors,” vol. 9434. Springer, pp. 3–18, 2015. Ray R, Gurung A, Das B, Bartocci E, Bogomolov S, Grosu R. XSpeed: Accelerating reachability analysis on multi-core processors. 2015;9434:3-18. doi:<a href="https://doi.org/10.1007/978-3-319-26287-1_1">10.1007/978-3-319-26287-1_1</a> R. Ray, A. Gurung, B. Das, E. Bartocci, S. Bogomolov, R. Grosu, 9434 (2015) 3–18. Ray, Rajarshi, et al. <i>XSpeed: Accelerating Reachability Analysis on Multi-Core Processors</i>. Vol. 9434, Springer, 2015, pp. 3–18, doi:<a href="https://doi.org/10.1007/978-3-319-26287-1_1">10.1007/978-3-319-26287-1_1</a>. Ray, R., Gurung, A., Das, B., Bartocci, E., Bogomolov, S., &#38; Grosu, R. (2015). XSpeed: Accelerating reachability analysis on multi-core processors. Presented at the HVC: Haifa Verification Conference, Haifa, Israel: Springer. <a href="https://doi.org/10.1007/978-3-319-26287-1_1">https://doi.org/10.1007/978-3-319-26287-1_1</a> 15412018-12-11T11:52:37Z2025-04-15T06:26:02Z