---
res:
  bibo_abstract:
  - 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.@eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Amit
      foaf_name: Gurung, Amit
      foaf_surname: Gurung
  - foaf_Person:
      foaf_givenName: Arup
      foaf_name: Deka, Arup
      foaf_surname: Deka
  - foaf_Person:
      foaf_givenName: Ezio
      foaf_name: Bartocci, Ezio
      foaf_surname: Bartocci
  - foaf_Person:
      foaf_givenName: Sergiy
      foaf_name: Bogomolov, Sergiy
      foaf_surname: Bogomolov
      foaf_workInfoHomepage: http://www.librecat.org/personId=369D9A44-F248-11E8-B48F-1D18A9856A87
    orcid: 0000-0002-0686-0365
  - foaf_Person:
      foaf_givenName: Radu
      foaf_name: Grosu, Radu
      foaf_surname: Grosu
  - foaf_Person:
      foaf_givenName: Rajarshi
      foaf_name: Ray, Rajarshi
      foaf_surname: Ray
  bibo_doi: 10.1109/MEMCOD.2016.7797741
  dct_date: 2016^xs_gYear
  dct_language: eng
  dct_publisher: IEEE@
  dct_title: Parallel reachability analysis for hybrid systems@
...