---
_id: '12171'
abstract:
- lang: eng
  text: 'We propose an algorithmic approach for synthesizing linear hybrid automata
    from time-series data. Unlike existing approaches, our approach provides a whole
    family of models with the same discrete structure but different dynamics. Each
    model in the family is guaranteed to capture the input data up to a precision
    error ε, in the following sense: For each time series, the model contains an execution
    that is ε-close to the data points. Our construction allows to effectively choose
    a model from this family with minimal precision error ε. We demonstrate the algorithm’s
    efficiency and its ability to find precise models in two case studies.'
acknowledgement: This work was supported in part by the European Union’s Horizon 2020
  research and innovation programme under the Marie Skłodowska-Curie grant agreement
  no. 847635, by the ERC-2020-AdG 101020093, by DIREC - Digital Research Centre Denmark,
  and by the Villum Investigator Grant S4OS.
alternative_title:
- LNCS
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 parametric hybrid automata
    from time series. In: <i>20th International Symposium on Automated Technology
    for Verification and Analysis</i>. Vol 13505. Springer Nature; 2022:337-353. doi:<a
    href="https://doi.org/10.1007/978-3-031-19992-9_22">10.1007/978-3-031-19992-9_22</a>'
  apa: 'Garcia Soto, M., Henzinger, T. A., &#38; Schilling, C. (2022). Synthesis of parametric
    hybrid automata from time series. In <i>20th International Symposium on Automated
    Technology for Verification and Analysis</i> (Vol. 13505, pp. 337–353). Virtual:
    Springer Nature. <a href="https://doi.org/10.1007/978-3-031-19992-9_22">https://doi.org/10.1007/978-3-031-19992-9_22</a>'
  chicago: Garcia Soto, Miriam, Thomas A Henzinger, and Christian Schilling. “Synthesis
    of Parametric Hybrid Automata from Time Series.” In <i>20th International Symposium
    on Automated Technology for Verification and Analysis</i>, 13505:337–53. Springer
    Nature, 2022. <a href="https://doi.org/10.1007/978-3-031-19992-9_22">https://doi.org/10.1007/978-3-031-19992-9_22</a>.
  ieee: M. Garcia Soto, T. A. Henzinger, and C. Schilling, “Synthesis of parametric
    hybrid automata from time series,” in <i>20th International Symposium on Automated
    Technology for Verification and Analysis</i>, Virtual, 2022, vol. 13505, pp. 337–353.
  ista: 'Garcia Soto M, Henzinger TA, Schilling C. 2022. Synthesis of parametric hybrid
    automata from time series. 20th International Symposium on Automated Technology
    for Verification and Analysis. ATVA: Automated Technology for Verification and
    Analysis, LNCS, vol. 13505, 337–353.'
  mla: Garcia Soto, Miriam, et al. “Synthesis of Parametric Hybrid Automata from Time
    Series.” <i>20th International Symposium on Automated Technology for Verification
    and Analysis</i>, vol. 13505, Springer Nature, 2022, pp. 337–53, doi:<a href="https://doi.org/10.1007/978-3-031-19992-9_22">10.1007/978-3-031-19992-9_22</a>.
  short: M. Garcia Soto, T.A. Henzinger, C. Schilling, in:, 20th International Symposium
    on Automated Technology for Verification and Analysis, Springer Nature, 2022,
    pp. 337–353.
conference:
  end_date: 2022-10-28
  location: Virtual
  name: 'ATVA: Automated Technology for Verification and Analysis'
  start_date: 2022-10-25
date_created: 2023-01-12T12:11:16Z
date_published: 2022-10-21T00:00:00Z
date_updated: 2023-02-13T09:27:55Z
day: '21'
department:
- _id: ToHe
doi: 10.1007/978-3-031-19992-9_22
ec_funded: 1
external_id:
  arxiv:
  - '2208.06383'
intvolume: '     13505'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.48550/arXiv.2208.06383
month: '10'
oa: 1
oa_version: Preprint
page: 337-353
project:
- _id: 62781420-2b32-11ec-9570-8d9b63373d4d
  call_identifier: H2020
  grant_number: '101020093'
  name: Vigilant Algorithmic Monitoring of Software
publication: 20th International Symposium on Automated Technology for Verification
  and Analysis
publication_identifier:
  eisbn:
  - '9783031199929'
  eissn:
  - 1611-3349
  isbn:
  - '9783031199912'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Synthesis of parametric hybrid automata from time series
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13505
year: '2022'
...
---
_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: International
    Conference on 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: International Conference on Hybrid Systems Computation and Control'
  start_date: 2021-05-19
date_created: 2021-02-26T16:30:39Z
date_published: 2021-05-01T00:00:00Z
date_updated: 2023-08-07T13:49:33Z
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
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: The Wittgenstein Prize
- _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: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
year: '2021'
...
---
_id: '7426'
abstract:
- lang: eng
  text: This paper presents a novel abstraction technique for analyzing Lyapunov and
    asymptotic stability of polyhedral switched systems. A polyhedral switched system
    is a hybrid system in which the continuous dynamics is specified by polyhedral
    differential inclusions, the invariants and guards are specified by polyhedral
    sets and the switching between the modes do not involve reset of variables. A
    finite state weighted graph abstracting the polyhedral switched system is constructed
    from a finite partition of the state–space, such that the satisfaction of certain
    graph conditions, such as the absence of cycles with product of weights on the
    edges greater than (or equal) to 1, implies the stability of the system. However,
    the graph is in general conservative and hence, the violation of the graph conditions
    does not imply instability. If the analysis fails to establish stability due to
    the conservativeness in the approximation, a counterexample (cycle with product
    of edge weights greater than or equal to 1) indicating a potential reason for
    the failure is returned. Further, a more precise approximation of the switched
    system can be constructed by considering a finer partition of the state–space
    in the construction of the finite weighted graph. We present experimental results
    on analyzing stability of switched systems using the above method.
article_number: '100856'
article_processing_charge: No
article_type: original
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: Pavithra
  full_name: Prabhakar, Pavithra
  last_name: Prabhakar
citation:
  ama: 'Garcia Soto M, Prabhakar P. Abstraction based verification of stability of
    polyhedral switched systems. <i>Nonlinear Analysis: Hybrid Systems</i>. 2020;36(5).
    doi:<a href="https://doi.org/10.1016/j.nahs.2020.100856">10.1016/j.nahs.2020.100856</a>'
  apa: 'Garcia Soto, M., &#38; Prabhakar, P. (2020). Abstraction based verification
    of stability of polyhedral switched systems. <i>Nonlinear Analysis: Hybrid Systems</i>.
    Elsevier. <a href="https://doi.org/10.1016/j.nahs.2020.100856">https://doi.org/10.1016/j.nahs.2020.100856</a>'
  chicago: 'Garcia Soto, Miriam, and Pavithra Prabhakar. “Abstraction Based Verification
    of Stability of Polyhedral Switched Systems.” <i>Nonlinear Analysis: Hybrid Systems</i>.
    Elsevier, 2020. <a href="https://doi.org/10.1016/j.nahs.2020.100856">https://doi.org/10.1016/j.nahs.2020.100856</a>.'
  ieee: 'M. Garcia Soto and P. Prabhakar, “Abstraction based verification of stability
    of polyhedral switched systems,” <i>Nonlinear Analysis: Hybrid Systems</i>, vol.
    36, no. 5. Elsevier, 2020.'
  ista: 'Garcia Soto M, Prabhakar P. 2020. Abstraction based verification of stability
    of polyhedral switched systems. Nonlinear Analysis: Hybrid Systems. 36(5), 100856.'
  mla: 'Garcia Soto, Miriam, and Pavithra Prabhakar. “Abstraction Based Verification
    of Stability of Polyhedral Switched Systems.” <i>Nonlinear Analysis: Hybrid Systems</i>,
    vol. 36, no. 5, 100856, Elsevier, 2020, doi:<a href="https://doi.org/10.1016/j.nahs.2020.100856">10.1016/j.nahs.2020.100856</a>.'
  short: 'M. Garcia Soto, P. Prabhakar, Nonlinear Analysis: Hybrid Systems 36 (2020).'
date_created: 2020-02-02T23:00:59Z
date_published: 2020-05-01T00:00:00Z
date_updated: 2023-08-17T14:32:54Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1016/j.nahs.2020.100856
external_id:
  isi:
  - '000528828600003'
file:
- access_level: open_access
  checksum: 560abfddb53f9fe921b6744f59f2cfaa
  content_type: application/pdf
  creator: dernst
  date_created: 2020-10-21T13:16:45Z
  date_updated: 2022-05-16T22:30:04Z
  embargo: 2022-05-15
  file_id: '8688'
  file_name: 2020_NAHS_GarciaSoto.pdf
  file_size: 818774
  relation: main_file
file_date_updated: 2022-05-16T22:30:04Z
has_accepted_license: '1'
intvolume: '        36'
isi: 1
issue: '5'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Submitted Version
project:
- _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: The Wittgenstein Prize
publication: 'Nonlinear Analysis: Hybrid Systems'
publication_identifier:
  issn:
  - 1751-570X
publication_status: published
publisher: Elsevier
quality_controlled: '1'
scopus_import: '1'
status: public
title: Abstraction based verification of stability of polyhedral switched systems
tmp:
  image: /images/cc_by_nc_nd.png
  legal_code_url: https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode
  name: Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International
    (CC BY-NC-ND 4.0)
  short: CC BY-NC-ND (4.0)
type: journal_article
user_id: 4359f0d1-fa6c-11eb-b949-802e58b17ae8
volume: 36
year: '2020'
...
---
_id: '9202'
abstract:
- lang: eng
  text: We propose a novel hybridization method for stability analysis that over-approximates
    nonlinear dynamical systems by switched systems with linear inclusion dynamics.
    We observe that existing hybridization techniques for safety analysis that over-approximate
    nonlinear dynamical systems by switched affine inclusion dynamics and provide
    fixed approximation error, do not suffice for stability analysis. Hence, we propose
    a hybridization method that provides a state-dependent error which converges to
    zero as the state tends to the equilibrium point. The crux of our hybridization
    computation is an elegant recursive algorithm that uses partial derivatives of
    a given function to obtain upper and lower bound matrices for the over-approximating
    linear inclusion. We illustrate our method on some examples to demonstrate the
    application of the theory for stability analysis. In particular, our method is
    able to establish stability of a nonlinear system which does not admit a polynomial
    Lyapunov function.
acknowledgement: Miriam Garc´ıa Soto was partially supported by the Austrian Science
  Fund (FWF) under grant Z211-N23 (Wittgenstein Award). Pavithra Prabhakar was partially
  supported by NSF CAREER Award No. 1552668, NSF Award No. 2008957 and ONR YIP Award
  No. N000141712577.
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: Pavithra
  full_name: Prabhakar, Pavithra
  last_name: Prabhakar
citation:
  ama: 'Garcia Soto M, Prabhakar P. Hybridization for stability verification of nonlinear
    switched systems. In: <i>2020 IEEE Real-Time Systems Symposium</i>. IEEE; 2020:244-256.
    doi:<a href="https://doi.org/10.1109/RTSS49844.2020.00031">10.1109/RTSS49844.2020.00031</a>'
  apa: 'Garcia Soto, M., &#38; Prabhakar, P. (2020). Hybridization for stability verification
    of nonlinear switched systems. In <i>2020 IEEE Real-Time Systems Symposium</i>
    (pp. 244–256). Houston, TX, USA : IEEE. <a href="https://doi.org/10.1109/RTSS49844.2020.00031">https://doi.org/10.1109/RTSS49844.2020.00031</a>'
  chicago: Garcia Soto, Miriam, and Pavithra Prabhakar. “Hybridization for Stability
    Verification of Nonlinear Switched Systems.” In <i>2020 IEEE Real-Time Systems
    Symposium</i>, 244–56. IEEE, 2020. <a href="https://doi.org/10.1109/RTSS49844.2020.00031">https://doi.org/10.1109/RTSS49844.2020.00031</a>.
  ieee: M. Garcia Soto and P. Prabhakar, “Hybridization for stability verification
    of nonlinear switched systems,” in <i>2020 IEEE Real-Time Systems Symposium</i>,
    Houston, TX, USA , 2020, pp. 244–256.
  ista: 'Garcia Soto M, Prabhakar P. 2020. Hybridization for stability verification
    of nonlinear switched systems. 2020 IEEE Real-Time Systems Symposium. RTTS: Real-Time
    Systems Symposium, 244–256.'
  mla: Garcia Soto, Miriam, and Pavithra Prabhakar. “Hybridization for Stability Verification
    of Nonlinear Switched Systems.” <i>2020 IEEE Real-Time Systems Symposium</i>,
    IEEE, 2020, pp. 244–56, doi:<a href="https://doi.org/10.1109/RTSS49844.2020.00031">10.1109/RTSS49844.2020.00031</a>.
  short: M. Garcia Soto, P. Prabhakar, in:, 2020 IEEE Real-Time Systems Symposium,
    IEEE, 2020, pp. 244–256.
conference:
  end_date: 2020-12-04
  location: 'Houston, TX, USA '
  name: 'RTTS: Real-Time Systems Symposium'
  start_date: 2020-12-01
date_created: 2021-02-26T16:38:24Z
date_published: 2020-12-01T00:00:00Z
date_updated: 2024-02-22T13:25:19Z
day: '01'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1109/RTSS49844.2020.00031
external_id:
  isi:
  - '000680435100021'
file:
- access_level: open_access
  checksum: 8f97f229316c3b3a6f0cf99297aa0941
  content_type: application/pdf
  creator: mgarcias
  date_created: 2021-02-26T16:38:14Z
  date_updated: 2021-02-26T16:38:14Z
  file_id: '9203'
  file_name: main.pdf
  file_size: 1125794
  relation: main_file
file_date_updated: 2021-02-26T16:38:14Z
has_accepted_license: '1'
isi: 1
language:
- iso: eng
month: '12'
oa: 1
oa_version: Submitted Version
page: 244-256
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
publication: 2020 IEEE Real-Time Systems Symposium
publication_identifier:
  eisbn:
  - '9781728183244'
  eissn:
  - 2576-3172
publication_status: published
publisher: IEEE
quality_controlled: '1'
status: public
title: Hybridization for stability verification of nonlinear switched systems
type: conference
user_id: 3E5EF7F0-F248-11E8-B48F-1D18A9856A87
year: '2020'
...
---
_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
date_created: 2019-05-27T07:09:53Z
date_published: 2019-07-12T00:00:00Z
date_updated: 2023-08-25T10:40:41Z
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: The Wittgenstein Prize
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'
...
---
_id: '6565'
abstract:
- lang: eng
  text: In this paper, we address the problem of synthesizing periodic switching controllers
    for stabilizing a family of linear systems. Our broad approach consists of constructing
    a finite game graph based on the family of linear systems such that every winning
    strategy on the game graph corresponds to a stabilizing switching controller for
    the family of linear systems. The construction of a (finite) game graph, the synthesis
    of a winning strategy and the extraction of a stabilizing controller are all computationally
    feasible. We illustrate our method on an example.
article_number: '8715598'
article_processing_charge: No
author:
- first_name: Atreyee
  full_name: Kundu, Atreyee
  last_name: Kundu
- 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: Pavithra
  full_name: Prabhakar, Pavithra
  last_name: Prabhakar
citation:
  ama: 'Kundu A, Garcia Soto M, Prabhakar P. Formal synthesis of stabilizing controllers
    for periodically controlled linear switched systems. In: <i>5th Indian Control
    Conference Proceedings</i>. IEEE; 2019. doi:<a href="https://doi.org/10.1109/INDIANCC.2019.8715598">10.1109/INDIANCC.2019.8715598</a>'
  apa: 'Kundu, A., Garcia Soto, M., &#38; Prabhakar, P. (2019). Formal synthesis of
    stabilizing controllers for periodically controlled linear switched systems. In
    <i>5th Indian Control Conference Proceedings</i>. Delhi, India: IEEE. <a href="https://doi.org/10.1109/INDIANCC.2019.8715598">https://doi.org/10.1109/INDIANCC.2019.8715598</a>'
  chicago: Kundu, Atreyee, Miriam Garcia Soto, and Pavithra Prabhakar. “Formal Synthesis
    of Stabilizing Controllers for Periodically Controlled Linear Switched Systems.”
    In <i>5th Indian Control Conference Proceedings</i>. IEEE, 2019. <a href="https://doi.org/10.1109/INDIANCC.2019.8715598">https://doi.org/10.1109/INDIANCC.2019.8715598</a>.
  ieee: A. Kundu, M. Garcia Soto, and P. Prabhakar, “Formal synthesis of stabilizing
    controllers for periodically controlled linear switched systems,” in <i>5th Indian
    Control Conference Proceedings</i>, Delhi, India, 2019.
  ista: Kundu A, Garcia Soto M, Prabhakar P. 2019. Formal synthesis of stabilizing
    controllers for periodically controlled linear switched systems. 5th Indian Control
    Conference Proceedings. ICC 2019 - Indian Control Conference, 8715598.
  mla: Kundu, Atreyee, et al. “Formal Synthesis of Stabilizing Controllers for Periodically
    Controlled Linear Switched Systems.” <i>5th Indian Control Conference Proceedings</i>,
    8715598, IEEE, 2019, doi:<a href="https://doi.org/10.1109/INDIANCC.2019.8715598">10.1109/INDIANCC.2019.8715598</a>.
  short: A. Kundu, M. Garcia Soto, P. Prabhakar, in:, 5th Indian Control Conference
    Proceedings, IEEE, 2019.
conference:
  end_date: 2019-01-11
  location: Delhi, India
  name: ICC 2019 - Indian Control Conference
  start_date: 2019-01-09
date_created: 2019-06-17T06:57:33Z
date_published: 2019-05-16T00:00:00Z
date_updated: 2021-01-12T08:08:01Z
day: '16'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1109/INDIANCC.2019.8715598
file:
- access_level: open_access
  checksum: d622a91af1e427f6b1e0ba8e18a2b767
  content_type: application/pdf
  creator: dernst
  date_created: 2020-10-21T13:13:49Z
  date_updated: 2020-10-21T13:13:49Z
  file_id: '8687'
  file_name: 2019_ICC_Kundu.pdf
  file_size: 396031
  relation: main_file
  success: 1
file_date_updated: 2020-10-21T13:13:49Z
has_accepted_license: '1'
language:
- iso: eng
month: '05'
oa: 1
oa_version: Submitted Version
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: The Wittgenstein Prize
publication: 5th Indian Control Conference Proceedings
publication_identifier:
  isbn:
  - 978-153866246-5
publication_status: published
publisher: IEEE
quality_controlled: '1'
scopus_import: '1'
status: public
title: Formal synthesis of stabilizing controllers for periodically controlled linear
  switched systems
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2019'
...