---
_id: '1541'
abstract:
- lang: eng
text: 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.
acknowledgement: This work was supported in part by the European Research Council
(ERC) under grant 267989 (QUAREM) and by the Austrian Science Fund (FWF) under grants
S11402-N23, S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).
alternative_title:
- LNCS
author:
- first_name: Rajarshi
full_name: Ray, Rajarshi
last_name: Ray
- first_name: Amit
full_name: Gurung, Amit
last_name: Gurung
- first_name: Binayak
full_name: Das, Binayak
last_name: Das
- first_name: Ezio
full_name: Bartocci, Ezio
last_name: Bartocci
- first_name: Sergiy
full_name: Bogomolov, Sergiy
id: 369D9A44-F248-11E8-B48F-1D18A9856A87
last_name: Bogomolov
orcid: 0000-0002-0686-0365
- first_name: Radu
full_name: Grosu, Radu
last_name: Grosu
citation:
ama: '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:10.1007/978-3-319-26287-1_1'
apa: 'Ray, R., Gurung, A., Das, B., Bartocci, E., Bogomolov, S., & Grosu, R.
(2015). XSpeed: Accelerating reachability analysis on multi-core processors. Presented
at the HVC: Haifa Verification Conference, Haifa, Israel: Springer. https://doi.org/10.1007/978-3-319-26287-1_1'
chicago: '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. https://doi.org/10.1007/978-3-319-26287-1_1.'
ieee: '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.'
ista: 'Ray R, Gurung A, Das B, Bartocci E, Bogomolov S, Grosu R. 2015. XSpeed: Accelerating
reachability analysis on multi-core processors. 9434, 3–18.'
mla: 'Ray, Rajarshi, et al. XSpeed: Accelerating Reachability Analysis on Multi-Core
Processors. Vol. 9434, Springer, 2015, pp. 3–18, doi:10.1007/978-3-319-26287-1_1.'
short: R. Ray, A. Gurung, B. Das, E. Bartocci, S. Bogomolov, R. Grosu, 9434 (2015)
3–18.
conference:
end_date: 2015-11-19
location: Haifa, Israel
name: 'HVC: Haifa Verification Conference'
start_date: 2015-11-17
date_created: 2018-12-11T11:52:37Z
date_published: 2015-11-28T00:00:00Z
date_updated: 2020-08-11T10:09:17Z
day: '28'
department:
- _id: ToHe
doi: 10.1007/978-3-319-26287-1_1
ec_funded: 1
intvolume: ' 9434'
language:
- iso: eng
month: '11'
oa_version: None
page: 3 - 18
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '267989'
name: Quantitative Reactive Modeling
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S11402-N23
name: Moderne Concurrency Paradigms
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: Z211
name: The Wittgenstein Prize
publication_status: published
publisher: Springer
publist_id: '5630'
quality_controlled: '1'
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: 'XSpeed: Accelerating reachability analysis on multi-core processors'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9434
year: '2015'
...