---
_id: '7231'
abstract:
- lang: eng
  text: Piecewise Barrier Tubes (PBT) is a new technique for flowpipe overapproximation
    for nonlinear systems with polynomial dynamics, which leverages a combination
    of barrier certificates. PBT has advantages over traditional time-step based methods
    in dealing with those nonlinear dynamical systems in which there is a large difference
    in speed between trajectories, producing an overapproximation that is time independent.
    However, the existing approach for PBT is not efficient due to the application
    of interval methods for enclosure-box computation, and it can only deal with continuous
    dynamical systems without uncertainty. In this paper, we extend the approach with
    the ability to handle both continuous and hybrid dynamical systems with uncertainty
    that can reside in parameters and/or noise. We also improve the efficiency of
    the method significantly, by avoiding the use of interval-based methods for the
    enclosure-box computation without loosing soundness. We have developed a C++ prototype
    implementing the proposed approach and we evaluate it on several benchmarks. The
    experiments show that our approach is more efficient and precise than other methods
    in the literature.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Hui
  full_name: Kong, Hui
  id: 3BDE25AA-F248-11E8-B48F-1D18A9856A87
  last_name: Kong
  orcid: 0000-0002-3066-6941
- first_name: Ezio
  full_name: Bartocci, Ezio
  last_name: Bartocci
- first_name: Yu
  full_name: Jiang, Yu
  last_name: Jiang
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
citation:
  ama: 'Kong H, Bartocci E, Jiang Y, Henzinger TA. Piecewise robust barrier tubes
    for nonlinear hybrid systems with uncertainty. In: <i>17th International Conference
    on Formal Modeling and Analysis of Timed Systems</i>. Vol 11750. Springer Nature;
    2019:123-141. doi:<a href="https://doi.org/10.1007/978-3-030-29662-9_8">10.1007/978-3-030-29662-9_8</a>'
  apa: 'Kong, H., Bartocci, E., Jiang, Y., &#38; Henzinger, T. A. (2019). Piecewise
    robust barrier tubes for nonlinear hybrid systems with uncertainty. In <i>17th
    International Conference on Formal Modeling and Analysis of Timed Systems</i>
    (Vol. 11750, pp. 123–141). Amsterdam, The Netherlands: Springer Nature. <a href="https://doi.org/10.1007/978-3-030-29662-9_8">https://doi.org/10.1007/978-3-030-29662-9_8</a>'
  chicago: Kong, Hui, Ezio Bartocci, Yu Jiang, and Thomas A Henzinger. “Piecewise
    Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty.” In <i>17th
    International Conference on Formal Modeling and Analysis of Timed Systems</i>,
    11750:123–41. Springer Nature, 2019. <a href="https://doi.org/10.1007/978-3-030-29662-9_8">https://doi.org/10.1007/978-3-030-29662-9_8</a>.
  ieee: H. Kong, E. Bartocci, Y. Jiang, and T. A. Henzinger, “Piecewise robust barrier
    tubes for nonlinear hybrid systems with uncertainty,” in <i>17th International
    Conference on Formal Modeling and Analysis of Timed Systems</i>, Amsterdam, The
    Netherlands, 2019, vol. 11750, pp. 123–141.
  ista: 'Kong H, Bartocci E, Jiang Y, Henzinger TA. 2019. Piecewise robust barrier
    tubes for nonlinear hybrid systems with uncertainty. 17th International Conference
    on Formal Modeling and Analysis of Timed Systems. FORMATS: Formal Modeling and
    Analysis of Timed Systems, LNCS, vol. 11750, 123–141.'
  mla: Kong, Hui, et al. “Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems
    with Uncertainty.” <i>17th International Conference on Formal Modeling and Analysis
    of Timed Systems</i>, vol. 11750, Springer Nature, 2019, pp. 123–41, doi:<a href="https://doi.org/10.1007/978-3-030-29662-9_8">10.1007/978-3-030-29662-9_8</a>.
  short: H. Kong, E. Bartocci, Y. Jiang, T.A. Henzinger, in:, 17th International Conference
    on Formal Modeling and Analysis of Timed Systems, Springer Nature, 2019, pp. 123–141.
conference:
  end_date: 2019-08-29
  location: Amsterdam, The Netherlands
  name: 'FORMATS: Formal Modeling and Analysis of Timed Systems'
  start_date: 2019-08-27
date_created: 2020-01-05T23:00:47Z
date_published: 2019-08-13T00:00:00Z
date_updated: 2025-04-15T06:26:06Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-030-29662-9_8
external_id:
  arxiv:
  - '1907.11514'
  isi:
  - '000611677700008'
intvolume: '     11750'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://arxiv.org/abs/1907.11514
month: '08'
oa: 1
oa_version: Preprint
page: 123-141
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
- _id: 25863FF4-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11407
  name: Game Theory
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: Formal methods for the design and analysis of complex systems
publication: 17th International Conference on Formal Modeling and Analysis of Timed
  Systems
publication_identifier:
  eissn:
  - 1611-3349
  isbn:
  - 978-3-0302-9661-2
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 11750
year: '2019'
...
---
_id: '7232'
abstract:
- lang: eng
  text: 'We present Mixed-time Signal Temporal Logic (STL−MX), a specification formalism
    which extends STL by capturing the discrete/ continuous time duality found in
    many cyber-physical systems (CPS), as well as mixed-signal electronic designs.
    In STL−MX, properties of components with continuous dynamics are expressed in
    STL, while specifications of components with discrete dynamics are written in
    LTL. To combine the two layers, we evaluate formulas on two traces, discrete-
    and continuous-time, and introduce two interface operators that map signals, properties
    and their satisfaction signals across the two time domains. We show that STL-mx
    has the expressive power of STL supplemented with an implicit T-periodic clock
    signal. We develop and implement an algorithm for monitoring STL-mx formulas and
    illustrate the approach using a mixed-signal example. '
alternative_title:
- LNCS
article_processing_charge: No
author:
- 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: Dejan
  full_name: Nickovic, Dejan
  id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
  last_name: Nickovic
citation:
  ama: 'Ferrere T, Maler O, Nickovic D. Mixed-time signal temporal logic. In: <i>17th
    International Conference on Formal Modeling and Analysis of Timed Systems</i>.
    Vol 11750. Springer Nature; 2019:59-75. doi:<a href="https://doi.org/10.1007/978-3-030-29662-9_4">10.1007/978-3-030-29662-9_4</a>'
  apa: 'Ferrere, T., Maler, O., &#38; Nickovic, D. (2019). Mixed-time signal temporal
    logic. In <i>17th International Conference on Formal Modeling and Analysis of
    Timed Systems</i> (Vol. 11750, pp. 59–75). Amsterdam, The Netherlands: Springer
    Nature. <a href="https://doi.org/10.1007/978-3-030-29662-9_4">https://doi.org/10.1007/978-3-030-29662-9_4</a>'
  chicago: Ferrere, Thomas, Oded Maler, and Dejan Nickovic. “Mixed-Time Signal Temporal
    Logic.” In <i>17th International Conference on Formal Modeling and Analysis of
    Timed Systems</i>, 11750:59–75. Springer Nature, 2019. <a href="https://doi.org/10.1007/978-3-030-29662-9_4">https://doi.org/10.1007/978-3-030-29662-9_4</a>.
  ieee: T. Ferrere, O. Maler, and D. Nickovic, “Mixed-time signal temporal logic,”
    in <i>17th International Conference on Formal Modeling and Analysis of Timed Systems</i>,
    Amsterdam, The Netherlands, 2019, vol. 11750, pp. 59–75.
  ista: 'Ferrere T, Maler O, Nickovic D. 2019. Mixed-time signal temporal logic. 17th
    International Conference on Formal Modeling and Analysis of Timed Systems. FORMATS:
    Formal Modeling and Anaysis of Timed Systems, LNCS, vol. 11750, 59–75.'
  mla: Ferrere, Thomas, et al. “Mixed-Time Signal Temporal Logic.” <i>17th International
    Conference on Formal Modeling and Analysis of Timed Systems</i>, vol. 11750, Springer
    Nature, 2019, pp. 59–75, doi:<a href="https://doi.org/10.1007/978-3-030-29662-9_4">10.1007/978-3-030-29662-9_4</a>.
  short: T. Ferrere, O. Maler, D. Nickovic, in:, 17th International Conference on
    Formal Modeling and Analysis of Timed Systems, Springer Nature, 2019, pp. 59–75.
conference:
  end_date: 2019-08-29
  location: Amsterdam, The Netherlands
  name: 'FORMATS: Formal Modeling and Anaysis of Timed Systems'
  start_date: 2019-08-27
date_created: 2020-01-05T23:00:48Z
date_published: 2019-08-13T00:00:00Z
date_updated: 2025-04-15T06:26:06Z
day: '13'
department:
- _id: ToHe
doi: 10.1007/978-3-030-29662-9_4
external_id:
  isi:
  - '000611677700004'
intvolume: '     11750'
isi: 1
language:
- iso: eng
month: '08'
oa_version: None
page: 59-75
project:
- _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: 17th International Conference on Formal Modeling and Analysis of Timed
  Systems
publication_identifier:
  eissn:
  - 1611-3349
  isbn:
  - 978-3-0302-9661-2
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Mixed-time signal temporal logic
type: conference
user_id: c635000d-4b10-11ee-a964-aac5a93f6ac1
volume: 11750
year: '2019'
...