---
_id: '647'
abstract:
- lang: eng
  text: Despite researchers’ efforts in the last couple of decades, reachability analysis
    is still a challenging problem even for linear hybrid systems. Among the existing
    approaches, the most practical ones are mainly based on bounded-time reachable
    set over-approximations. For the purpose of unbounded-time analysis, one important
    strategy is to abstract the original system and find an invariant for the abstraction.
    In this paper, we propose an approach to constructing a new kind of abstraction
    called conic abstraction for affine hybrid systems, and to computing reachable
    sets based on this abstraction. The essential feature of a conic abstraction is
    that it partitions the state space of a system into a set of convex polyhedral
    cones which is derived from a uniform conic partition of the derivative space.
    Such a set of polyhedral cones is able to cut all trajectories of the system into
    almost straight segments so that every segment of a reach pipe in a polyhedral
    cone tends to be straight as well, and hence can be over-approximated tightly
    by polyhedra using similar techniques as HyTech or PHAVer. In particular, for
    diagonalizable affine systems, our approach can guarantee to find an invariant
    for unbounded reachable sets, which is beyond the capability of bounded-time reachability
    analysis tools. We implemented the approach in a tool and experiments on benchmarks
    show that our approach is more powerful than SpaceEx and PHAVer in dealing with
    diagonalizable systems.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Sergiy
  full_name: Bogomolov, Sergiy
  id: 369D9A44-F248-11E8-B48F-1D18A9856A87
  last_name: Bogomolov
  orcid: 0000-0002-0686-0365
- first_name: Mirco
  full_name: Giacobbe, Mirco
  id: 3444EA5E-F248-11E8-B48F-1D18A9856A87
  last_name: Giacobbe
  orcid: 0000-0001-8180-0904
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Hui
  full_name: Kong, Hui
  id: 3BDE25AA-F248-11E8-B48F-1D18A9856A87
  last_name: Kong
  orcid: 0000-0002-3066-6941
citation:
  ama: 'Bogomolov S, Giacobbe M, Henzinger TA, Kong H. Conic abstractions for hybrid
    systems. In: Vol 10419. Springer; 2017:116-132. doi:<a href="https://doi.org/10.1007/978-3-319-65765-3_7">10.1007/978-3-319-65765-3_7</a>'
  apa: 'Bogomolov, S., Giacobbe, M., Henzinger, T. A., &#38; Kong, H. (2017). Conic
    abstractions for hybrid systems (Vol. 10419, pp. 116–132). Presented at the FORMATS:
    Formal Modelling and Analysis of Timed Systems, Berlin, Germany: Springer. <a
    href="https://doi.org/10.1007/978-3-319-65765-3_7">https://doi.org/10.1007/978-3-319-65765-3_7</a>'
  chicago: Bogomolov, Sergiy, Mirco Giacobbe, Thomas A Henzinger, and Hui Kong. “Conic
    Abstractions for Hybrid Systems,” 10419:116–32. Springer, 2017. <a href="https://doi.org/10.1007/978-3-319-65765-3_7">https://doi.org/10.1007/978-3-319-65765-3_7</a>.
  ieee: 'S. Bogomolov, M. Giacobbe, T. A. Henzinger, and H. Kong, “Conic abstractions
    for hybrid systems,” presented at the FORMATS: Formal Modelling and Analysis of
    Timed Systems, Berlin, Germany, 2017, vol. 10419, pp. 116–132.'
  ista: 'Bogomolov S, Giacobbe M, Henzinger TA, Kong H. 2017. Conic abstractions for
    hybrid systems. FORMATS: Formal Modelling and Analysis of Timed Systems, LNCS,
    vol. 10419, 116–132.'
  mla: Bogomolov, Sergiy, et al. <i>Conic Abstractions for Hybrid Systems</i>. Vol.
    10419, Springer, 2017, pp. 116–32, doi:<a href="https://doi.org/10.1007/978-3-319-65765-3_7">10.1007/978-3-319-65765-3_7</a>.
  short: S. Bogomolov, M. Giacobbe, T.A. Henzinger, H. Kong, in:, Springer, 2017,
    pp. 116–132.
conference:
  end_date: 2017-09-07
  location: Berlin, Germany
  name: 'FORMATS: Formal Modelling and Analysis of Timed Systems'
  start_date: 2017-09-05
corr_author: '1'
date_created: 2018-12-11T11:47:41Z
date_published: 2017-09-01T00:00:00Z
date_updated: 2026-04-08T07:47:13Z
day: '01'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-319-65765-3_7
external_id:
  isi:
  - '000611678300007'
file:
- access_level: open_access
  checksum: faf546914ba29bcf9974ee36b6b16750
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:12:38Z
  date_updated: 2020-07-14T12:47:31Z
  file_id: '4956'
  file_name: IST-2017-831-v1+1_main.pdf
  file_size: 3806864
  relation: main_file
file_date_updated: 2020-07-14T12:47:31Z
has_accepted_license: '1'
isi: 1
language:
- iso: eng
month: '09'
oa: 1
oa_version: Submitted Version
page: 116 - 132
project:
- _id: 25F5A88A-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Moderne Concurrency Paradigms
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: Formal methods for the design and analysis of complex systems
publication_identifier:
  isbn:
  - 978-331965764-6
publication_status: published
publisher: Springer
publist_id: '7129'
pubrep_id: '831'
quality_controlled: '1'
related_material:
  record:
  - id: '6894'
    relation: dissertation_contains
    status: public
scopus_import: '1'
status: public
title: Conic abstractions for hybrid systems
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: '10419 '
year: '2017'
...
