---
_id: '1103'
abstract:
- lang: eng
  text: We propose two parallel state-space-exploration algorithms for hybrid automaton
    (HA), with the goal of enhancing performance on multi-core shared-memory systems.
    The first uses the parallel, breadth-first-search algorithm (PBFS) of the SPIN
    model checker, when traversing the discrete modes of the HA, and enhances it with
    a parallel exploration of the continuous states within each mode. We show that
    this simple-minded extension of PBFS does not provide the desired load balancing
    in many HA benchmarks. The second algorithm is a task-parallel BFS algorithm (TP-BFS),
    which uses a cheap precomputation of the cost associated with the post operations
    (both continuous and discrete) in order to improve load balancing. We illustrate
    the TP-BFS and the cost precomputation of the post operators on a support-function-based
    algorithm for state-space exploration. The performance comparison of the two algorithms
    shows that, in general, TP-BFS provides a better utilization/load-balancing of
    the CPU. Both algorithms are implemented in the model checker XSpeed. Our experiments
    show a maximum speed-up of more than 2000 χ on a navigation benchmark, with respect
    to SpaceEx LGG scenario. In order to make the comparison fair, we employed an
    equal number of post operations in both tools. To the best of our knowledge, this
    paper represents the first attempt to provide parallel, reachability-analysis
    algorithms for HA.
acknowledgement: This work was supported in part by DST-SERB, GoI under Project No.
  YSS/2014/000623 and 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).
article_number: '7797741'
article_processing_charge: No
arxiv: 1
author:
- first_name: Amit
  full_name: Gurung, Amit
  last_name: Gurung
- first_name: Arup
  full_name: Deka, Arup
  last_name: Deka
- 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
- first_name: Rajarshi
  full_name: Ray, Rajarshi
  last_name: Ray
citation:
  ama: 'Gurung A, Deka A, Bartocci E, Bogomolov S, Grosu R, Ray R. Parallel reachability
    analysis for hybrid systems. In: IEEE; 2016. doi:<a href="https://doi.org/10.1109/MEMCOD.2016.7797741">10.1109/MEMCOD.2016.7797741</a>'
  apa: 'Gurung, A., Deka, A., Bartocci, E., Bogomolov, S., Grosu, R., &#38; Ray, R.
    (2016). Parallel reachability analysis for hybrid systems. Presented at the MEMOCODE:
    Conference on Formal Methods and Models for System Design, Kanpur, India : IEEE.
    <a href="https://doi.org/10.1109/MEMCOD.2016.7797741">https://doi.org/10.1109/MEMCOD.2016.7797741</a>'
  chicago: Gurung, Amit, Arup Deka, Ezio Bartocci, Sergiy Bogomolov, Radu Grosu, and
    Rajarshi Ray. “Parallel Reachability Analysis for Hybrid Systems.” IEEE, 2016.
    <a href="https://doi.org/10.1109/MEMCOD.2016.7797741">https://doi.org/10.1109/MEMCOD.2016.7797741</a>.
  ieee: 'A. Gurung, A. Deka, E. Bartocci, S. Bogomolov, R. Grosu, and R. Ray, “Parallel
    reachability analysis for hybrid systems,” presented at the MEMOCODE: Conference
    on Formal Methods and Models for System Design, Kanpur, India , 2016.'
  ista: 'Gurung A, Deka A, Bartocci E, Bogomolov S, Grosu R, Ray R. 2016. Parallel
    reachability analysis for hybrid systems. MEMOCODE: Conference on Formal Methods
    and Models for System Design, 7797741.'
  mla: Gurung, Amit, et al. <i>Parallel Reachability Analysis for Hybrid Systems</i>.
    7797741, IEEE, 2016, doi:<a href="https://doi.org/10.1109/MEMCOD.2016.7797741">10.1109/MEMCOD.2016.7797741</a>.
  short: A. Gurung, A. Deka, E. Bartocci, S. Bogomolov, R. Grosu, R. Ray, in:, IEEE,
    2016.
conference:
  end_date: 2016-11-20
  location: 'Kanpur, India '
  name: 'MEMOCODE: Conference on Formal Methods and Models for System Design'
  start_date: 2016-11-18
date_created: 2018-12-11T11:50:09Z
date_published: 2016-12-27T00:00:00Z
date_updated: 2025-06-04T11:52:29Z
day: '27'
department:
- _id: ToHe
doi: 10.1109/MEMCOD.2016.7797741
ec_funded: 1
external_id:
  arxiv:
  - '1606.05473'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1606.05473
month: '12'
oa: 1
oa_version: Preprint
project:
- _id: 25EE3708-B435-11E9-9278-68D0E5697425
  call_identifier: FP7
  grant_number: '267989'
  name: Quantitative Reactive Modeling
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: Formal methods for the design and analysis of complex systems
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
publication_status: published
publisher: IEEE
publist_id: '6272'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Parallel reachability analysis for hybrid systems
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2016'
...