---
_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:<a href="https://doi.org/10.1007/978-3-319-26287-1_1">10.1007/978-3-319-26287-1_1</a>'
  apa: '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>'
  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. <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>.'
  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. <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>.'
  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: 2025-04-15T06:26:02Z
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: Formal methods for the design and analysis of complex systems
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'
...