---
_id: '9200'
abstract:
- lang: eng
  text: Formal design of embedded and cyber-physical systems relies on mathematical
    modeling. In this paper, we consider the model class of hybrid automata whose
    dynamics are defined by affine differential equations. Given a set of time-series
    data, we present an algorithmic approach to synthesize a hybrid automaton exhibiting
    behavior that is close to the data, up to a specified precision, and changes in
    synchrony with the data. A fundamental problem in our synthesis algorithm is to
    check membership of a time series in a hybrid automaton. Our solution integrates
    reachability and optimization techniques for affine dynamical systems to obtain
    both a sufficient and a necessary condition for membership, combined in a refinement
    framework. The algorithm processes one time series at a time and hence can be
    interrupted, provide an intermediate result, and be resumed. We report experimental
    results demonstrating the applicability of our synthesis approach.
acknowledgement: This research was supported in part by the Austrian Science Fund
  (FWF) under grant Z211-N23 (Wittgenstein Award) and the European Union’s Horizon
  2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement
  No. 754411.
article_processing_charge: No
arxiv: 1
author:
- first_name: Miriam
  full_name: Garcia Soto, Miriam
  id: 4B3207F6-F248-11E8-B48F-1D18A9856A87
  last_name: Garcia Soto
  orcid: 0000-0003-2936-5719
- 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: Christian
  full_name: Schilling, Christian
  id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
  last_name: Schilling
  orcid: 0000-0003-3658-1065
citation:
  ama: 'Garcia Soto M, Henzinger TA, Schilling C. Synthesis of hybrid automata with
    affine dynamics from time-series data. In: <i>HSCC ’21: Proceedings of the 24th
    International Conference on Hybrid Systems: Computation and Control</i>. Association
    for Computing Machinery; 2021:2102.12734. doi:<a href="https://doi.org/10.1145/3447928.3456704">10.1145/3447928.3456704</a>'
  apa: 'Garcia Soto, M., Henzinger, T. A., &#38; Schilling, C. (2021). Synthesis of
    hybrid automata with affine dynamics from time-series data. In <i>HSCC ’21: Proceedings
    of the 24th International Conference on Hybrid Systems: Computation and Control</i>
    (p. 2102.12734). Nashville, TN, United States: Association for Computing Machinery.
    <a href="https://doi.org/10.1145/3447928.3456704">https://doi.org/10.1145/3447928.3456704</a>'
  chicago: 'Garcia Soto, Miriam, Thomas A Henzinger, and Christian Schilling. “Synthesis
    of Hybrid Automata with Affine Dynamics from Time-Series Data.” In <i>HSCC ’21:
    Proceedings of the 24th International Conference on Hybrid Systems: Computation
    and Control</i>, 2102.12734. Association for Computing Machinery, 2021. <a href="https://doi.org/10.1145/3447928.3456704">https://doi.org/10.1145/3447928.3456704</a>.'
  ieee: 'M. Garcia Soto, T. A. Henzinger, and C. Schilling, “Synthesis of hybrid automata
    with affine dynamics from time-series data,” in <i>HSCC ’21: Proceedings of the
    24th International Conference on Hybrid Systems: Computation and Control</i>,
    Nashville, TN, United States, 2021, p. 2102.12734.'
  ista: 'Garcia Soto M, Henzinger TA, Schilling C. 2021. Synthesis of hybrid automata
    with affine dynamics from time-series data. HSCC ’21: Proceedings of the 24th
    International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid
    Systems - Computation and Control, 2102.12734.'
  mla: 'Garcia Soto, Miriam, et al. “Synthesis of Hybrid Automata with Affine Dynamics
    from Time-Series Data.” <i>HSCC ’21: Proceedings of the 24th International Conference
    on Hybrid Systems: Computation and Control</i>, Association for Computing Machinery,
    2021, p. 2102.12734, doi:<a href="https://doi.org/10.1145/3447928.3456704">10.1145/3447928.3456704</a>.'
  short: 'M. Garcia Soto, T.A. Henzinger, C. Schilling, in:, HSCC ’21: Proceedings
    of the 24th International Conference on Hybrid Systems: Computation and Control,
    Association for Computing Machinery, 2021, p. 2102.12734.'
conference:
  end_date: 2021-05-21
  location: Nashville, TN, United States
  name: 'HSCC: Hybrid Systems - Computation and Control'
  start_date: 2021-05-19
corr_author: '1'
date_created: 2021-02-26T16:30:39Z
date_published: 2021-05-01T00:00:00Z
date_updated: 2025-07-10T12:01:40Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1145/3447928.3456704
ec_funded: 1
external_id:
  arxiv:
  - '2102.12734'
  isi:
  - '000932821700028'
file:
- access_level: open_access
  checksum: 4c1202c1abf71384c3ee6fea88c2f80e
  content_type: application/pdf
  creator: kschuh
  date_created: 2021-05-25T13:53:22Z
  date_updated: 2021-05-25T13:53:22Z
  file_id: '9424'
  file_name: 2021_HSCC_Soto.pdf
  file_size: 1474786
  relation: main_file
  success: 1
file_date_updated: 2021-05-25T13:53:22Z
has_accepted_license: '1'
isi: 1
keyword:
- hybrid automaton
- membership
- system identification
language:
- iso: eng
license: https://creativecommons.org/licenses/by/4.0/
month: '05'
oa: 1
oa_version: Published Version
page: '2102.12734'
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: Formal methods for the design and analysis of complex systems
- _id: 260C2330-B435-11E9-9278-68D0E5697425
  call_identifier: H2020
  grant_number: '754411'
  name: ISTplus - Postdoctoral Fellowships
publication: 'HSCC ''21: Proceedings of the 24th International Conference on Hybrid
  Systems: Computation and Control'
publication_identifier:
  isbn:
  - '9781450383394'
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: Synthesis of hybrid automata with affine dynamics from time-series data
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2021'
...
---
_id: '6493'
abstract:
- lang: eng
  text: We present two algorithmic approaches for synthesizing linear hybrid automata
    from experimental data. Unlike previous approaches, our algorithms work without
    a template and generate an automaton with nondeterministic guards and invariants,
    and with an arbitrary number and topology of modes. They thus construct a succinct
    model from the data and provide formal guarantees. In particular, (1) the generated
    automaton can reproduce the data up to a specified tolerance and (2) the automaton
    is tight, given the first guarantee. Our first approach encodes the synthesis
    problem as a logical formula in the theory of linear arithmetic, which can then
    be solved by an SMT solver. This approach minimizes the number of modes in the
    resulting model but is only feasible for limited data sets. To address scalability,
    we propose a second approach that does not enforce to find a minimal model. The
    algorithm constructs an initial automaton and then iteratively extends the automaton
    based on processing new data. Therefore the algorithm is well-suited for online
    and synthesis-in-the-loop applications. The core of the algorithm is a membership
    query that checks whether, within the specified tolerance, a given data set can
    result from the execution of a given automaton. We solve this membership problem
    for linear hybrid automata by repeated reachability computations. We demonstrate
    the effectiveness of the algorithm on synthetic data sets and on cardiac-cell
    measurements.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Miriam
  full_name: Garcia Soto, Miriam
  id: 4B3207F6-F248-11E8-B48F-1D18A9856A87
  last_name: Garcia Soto
  orcid: 0000−0003−2936−5719
- 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: Christian
  full_name: Schilling, Christian
  id: 3A2F4DCE-F248-11E8-B48F-1D18A9856A87
  last_name: Schilling
  orcid: 0000-0003-3658-1065
- first_name: Luka
  full_name: Zeleznik, Luka
  id: 3ADCA2E4-F248-11E8-B48F-1D18A9856A87
  last_name: Zeleznik
citation:
  ama: 'Garcia Soto M, Henzinger TA, Schilling C, Zeleznik L. Membership-based synthesis
    of linear hybrid automata. In: <i>31st International Conference on Computer-Aided
    Verification</i>. Vol 11561. Springer; 2019:297-314. doi:<a href="https://doi.org/10.1007/978-3-030-25540-4_16">10.1007/978-3-030-25540-4_16</a>'
  apa: 'Garcia Soto, M., Henzinger, T. A., Schilling, C., &#38; Zeleznik, L. (2019).
    Membership-based synthesis of linear hybrid automata. In <i>31st International
    Conference on Computer-Aided Verification</i> (Vol. 11561, pp. 297–314). New York
    City, NY, USA: Springer. <a href="https://doi.org/10.1007/978-3-030-25540-4_16">https://doi.org/10.1007/978-3-030-25540-4_16</a>'
  chicago: Garcia Soto, Miriam, Thomas A Henzinger, Christian Schilling, and Luka
    Zeleznik. “Membership-Based Synthesis of Linear Hybrid Automata.” In <i>31st International
    Conference on Computer-Aided Verification</i>, 11561:297–314. Springer, 2019.
    <a href="https://doi.org/10.1007/978-3-030-25540-4_16">https://doi.org/10.1007/978-3-030-25540-4_16</a>.
  ieee: M. Garcia Soto, T. A. Henzinger, C. Schilling, and L. Zeleznik, “Membership-based
    synthesis of linear hybrid automata,” in <i>31st International Conference on Computer-Aided
    Verification</i>, New York City, NY, USA, 2019, vol. 11561, pp. 297–314.
  ista: 'Garcia Soto M, Henzinger TA, Schilling C, Zeleznik L. 2019. Membership-based
    synthesis of linear hybrid automata. 31st International Conference on Computer-Aided
    Verification. CAV: Computer-Aided Verification, LNCS, vol. 11561, 297–314.'
  mla: Garcia Soto, Miriam, et al. “Membership-Based Synthesis of Linear Hybrid Automata.”
    <i>31st International Conference on Computer-Aided Verification</i>, vol. 11561,
    Springer, 2019, pp. 297–314, doi:<a href="https://doi.org/10.1007/978-3-030-25540-4_16">10.1007/978-3-030-25540-4_16</a>.
  short: M. Garcia Soto, T.A. Henzinger, C. Schilling, L. Zeleznik, in:, 31st International
    Conference on Computer-Aided Verification, Springer, 2019, pp. 297–314.
conference:
  end_date: 2019-07-18
  location: New York City, NY, USA
  name: 'CAV: Computer-Aided Verification'
  start_date: 2019-07-15
corr_author: '1'
date_created: 2019-05-27T07:09:53Z
date_published: 2019-07-12T00:00:00Z
date_updated: 2025-04-15T06:26:13Z
day: '12'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-030-25540-4_16
ec_funded: 1
external_id:
  isi:
  - '000491468000016'
file:
- access_level: open_access
  checksum: 1f1d61b83a151031745ef70a501da3d6
  content_type: application/pdf
  creator: dernst
  date_created: 2019-08-14T11:05:30Z
  date_updated: 2020-07-14T12:47:32Z
  file_id: '6817'
  file_name: 2019_CAV_GarciaSoto.pdf
  file_size: 674795
  relation: main_file
file_date_updated: 2020-07-14T12:47:32Z
has_accepted_license: '1'
intvolume: '     11561'
isi: 1
keyword:
- Synthesis
- Linear hybrid automaton
- Membership
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 297-314
project:
- _id: 260C2330-B435-11E9-9278-68D0E5697425
  call_identifier: H2020
  grant_number: '754411'
  name: ISTplus - Postdoctoral Fellowships
- _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: 31st International Conference on Computer-Aided Verification
publication_identifier:
  isbn:
  - '9783030255398'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
status: public
title: Membership-based synthesis of linear hybrid automata
tmp:
  image: /images/cc_by.png
  legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
  name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
  short: CC BY (4.0)
type: conference
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 11561
year: '2019'
...