---
_id: '636'
abstract:
- lang: eng
  text: Signal regular expressions can specify sequential properties of real-valued
    signals based on threshold conditions, regular operations, and duration constraints.
    In this paper we endow them with a quantitative semantics which indicates how
    robustly a signal matches or does not match a given expression. First, we show
    that this semantics is a safe approximation of a distance between the signal and
    the language defined by the expression. Then, we consider the robust matching
    problem, that is, computing the quantitative semantics of every segment of a given
    signal relative to an expression. We present an algorithm that solves this problem
    for piecewise-constant and piecewise-linear signals and show that for such signals
    the robustness map is a piecewise-linear function. The availability of an indicator
    describing how robustly a signal segment matches some regular pattern provides
    a general framework for quantitative monitoring of cyber-physical systems.
alternative_title:
- LNCS
author:
- first_name: Alexey
  full_name: Bakhirkin, Alexey
  last_name: Bakhirkin
- first_name: Thomas
  full_name: Ferrere, Thomas
  id: 40960E6E-F248-11E8-B48F-1D18A9856A87
  last_name: Ferrere
  orcid: 0000-0001-5199-3143
- first_name: Oded
  full_name: Maler, Oded
  last_name: Maler
- first_name: Dogan
  full_name: Ulus, Dogan
  last_name: Ulus
citation:
  ama: 'Bakhirkin A, Ferrere T, Maler O, Ulus D. On the quantitative semantics of
    regular expressions over real-valued signals. In: Abate A, Geeraerts G, eds. Vol
    10419. Springer; 2017:189-206. doi:<a href="https://doi.org/10.1007/978-3-319-65765-3_11">10.1007/978-3-319-65765-3_11</a>'
  apa: 'Bakhirkin, A., Ferrere, T., Maler, O., &#38; Ulus, D. (2017). On the quantitative
    semantics of regular expressions over real-valued signals. In A. Abate &#38; G.
    Geeraerts (Eds.) (Vol. 10419, pp. 189–206). 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_11">https://doi.org/10.1007/978-3-319-65765-3_11</a>'
  chicago: Bakhirkin, Alexey, Thomas Ferrere, Oded Maler, and Dogan Ulus. “On the
    Quantitative Semantics of Regular Expressions over Real-Valued Signals.” edited
    by Alessandro Abate and Gilles Geeraerts, 10419:189–206. Springer, 2017. <a href="https://doi.org/10.1007/978-3-319-65765-3_11">https://doi.org/10.1007/978-3-319-65765-3_11</a>.
  ieee: 'A. Bakhirkin, T. Ferrere, O. Maler, and D. Ulus, “On the quantitative semantics
    of regular expressions over real-valued signals,” presented at the FORMATS: Formal
    Modelling and Analysis of Timed Systems, Berlin, Germany, 2017, vol. 10419, pp.
    189–206.'
  ista: 'Bakhirkin A, Ferrere T, Maler O, Ulus D. 2017. On the quantitative semantics
    of regular expressions over real-valued signals. FORMATS: Formal Modelling and
    Analysis of Timed Systems, LNCS, vol. 10419, 189–206.'
  mla: Bakhirkin, Alexey, et al. <i>On the Quantitative Semantics of Regular Expressions
    over Real-Valued Signals</i>. Edited by Alessandro Abate and Gilles Geeraerts,
    vol. 10419, Springer, 2017, pp. 189–206, doi:<a href="https://doi.org/10.1007/978-3-319-65765-3_11">10.1007/978-3-319-65765-3_11</a>.
  short: A. Bakhirkin, T. Ferrere, O. Maler, D. Ulus, in:, A. Abate, G. Geeraerts
    (Eds.), Springer, 2017, pp. 189–206.
conference:
  end_date: 2017-09-07
  location: Berlin, Germany
  name: 'FORMATS: Formal Modelling and Analysis of Timed Systems'
  start_date: 2017-09-05
date_created: 2018-12-11T11:47:38Z
date_published: 2017-08-03T00:00:00Z
date_updated: 2021-01-12T08:07:14Z
day: '03'
department:
- _id: ToHe
doi: 10.1007/978-3-319-65765-3_11
editor:
- first_name: Alessandro
  full_name: Abate, Alessandro
  last_name: Abate
- first_name: Gilles
  full_name: Geeraerts, Gilles
  last_name: Geeraerts
intvolume: '     10419'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://hal.archives-ouvertes.fr/hal-01552132
month: '08'
oa: 1
oa_version: Submitted Version
page: 189 - 206
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: The Wittgenstein Prize
publication_identifier:
  isbn:
  - 978-331965764-6
publication_status: published
publisher: Springer
publist_id: '7152'
quality_controlled: '1'
scopus_import: 1
status: public
title: On the quantitative semantics of regular expressions over real-valued signals
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
volume: 10419
year: '2017'
...
---
_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
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
date_created: 2018-12-11T11:47:41Z
date_published: 2017-09-01T00:00:00Z
date_updated: 2023-09-07T12:53:00Z
day: '01'
ddc:
- '005'
department:
- _id: ToHe
doi: 10.1007/978-3-319-65765-3_7
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'
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: The Wittgenstein Prize
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: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: '10419 '
year: '2017'
...