---
_id: '6462'
abstract:
- lang: eng
  text: A controller is a device that interacts with a plant. At each time point,it
    reads the plant’s state and issues commands with the goal that the plant oper-ates
    optimally. Constructing optimal controllers is a fundamental and challengingproblem.
    Machine learning techniques have recently been successfully applied totrain controllers,
    yet they have limitations. Learned controllers are monolithic andhard to reason
    about. In particular, it is difficult to add features without retraining,to guarantee
    any level of performance, and to achieve acceptable performancewhen encountering
    untrained scenarios. These limitations can be addressed bydeploying quantitative
    run-timeshieldsthat serve as a proxy for the controller.At each time point, the
    shield reads the command issued by the controller andmay choose to alter it before
    passing it on to the plant. We show how optimalshields that interfere as little
    as possible while guaranteeing a desired level ofcontroller performance, can be
    generated systematically and automatically usingreactive  synthesis.  First,  we  abstract  the  plant  by  building  a  stochastic  model.Second,
    we consider the learned controller to be a black box. Third, we mea-surecontroller
    performanceandshield interferenceby two quantitative run-timemeasures that are
    formally defined using weighted automata. Then, the problemof constructing a shield
    that guarantees maximal performance with minimal inter-ference is the problem
    of finding an optimal strategy in a stochastic2-player game“controller versus
    shield” played on the abstract state space of the plant with aquantitative objective
    obtained from combining the performance and interferencemeasures. We illustrate
    the effectiveness of our approach by automatically con-structing lightweight shields
    for learned traffic-light controllers in various roadnetworks. The shields we
    generate avoid liveness bugs, improve controller per-formance in untrained and
    changing traffic situations, and add features to learnedcontrollers, such as giving
    priority to emergency vehicles.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Guy
  full_name: Avni, Guy
  id: 463C8BC2-F248-11E8-B48F-1D18A9856A87
  last_name: Avni
  orcid: 0000-0001-5588-8287
- first_name: Roderick
  full_name: Bloem, Roderick
  last_name: Bloem
- first_name: Krishnendu
  full_name: Chatterjee, Krishnendu
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- 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: Bettina
  full_name: Konighofer, Bettina
  last_name: Konighofer
- first_name: Stefan
  full_name: Pranger, Stefan
  last_name: Pranger
citation:
  ama: 'Avni G, Bloem R, Chatterjee K, Henzinger TA, Konighofer B, Pranger S. Run-time
    optimization for learned controllers through quantitative games. In: <i>31st International
    Conference on Computer-Aided Verification</i>. Vol 11561. Springer; 2019:630-649.
    doi:<a href="https://doi.org/10.1007/978-3-030-25540-4_36">10.1007/978-3-030-25540-4_36</a>'
  apa: 'Avni, G., Bloem, R., Chatterjee, K., Henzinger, T. A., Konighofer, B., &#38;
    Pranger, S. (2019). Run-time optimization for learned controllers through quantitative
    games. In <i>31st International Conference on Computer-Aided Verification</i>
    (Vol. 11561, pp. 630–649). New York, NY, United States: Springer. <a href="https://doi.org/10.1007/978-3-030-25540-4_36">https://doi.org/10.1007/978-3-030-25540-4_36</a>'
  chicago: Avni, Guy, Roderick Bloem, Krishnendu Chatterjee, Thomas A Henzinger, Bettina
    Konighofer, and Stefan Pranger. “Run-Time Optimization for Learned Controllers
    through Quantitative Games.” In <i>31st International Conference on Computer-Aided
    Verification</i>, 11561:630–49. Springer, 2019. <a href="https://doi.org/10.1007/978-3-030-25540-4_36">https://doi.org/10.1007/978-3-030-25540-4_36</a>.
  ieee: G. Avni, R. Bloem, K. Chatterjee, T. A. Henzinger, B. Konighofer, and S. Pranger,
    “Run-time optimization for learned controllers through quantitative games,” in
    <i>31st International Conference on Computer-Aided Verification</i>, New York,
    NY, United States, 2019, vol. 11561, pp. 630–649.
  ista: 'Avni G, Bloem R, Chatterjee K, Henzinger TA, Konighofer B, Pranger S. 2019.
    Run-time optimization for learned controllers through quantitative games. 31st
    International Conference on Computer-Aided Verification. CAV: Computer Aided Verification,
    LNCS, vol. 11561, 630–649.'
  mla: Avni, Guy, et al. “Run-Time Optimization for Learned Controllers through Quantitative
    Games.” <i>31st International Conference on Computer-Aided Verification</i>, vol.
    11561, Springer, 2019, pp. 630–49, doi:<a href="https://doi.org/10.1007/978-3-030-25540-4_36">10.1007/978-3-030-25540-4_36</a>.
  short: G. Avni, R. Bloem, K. Chatterjee, T.A. Henzinger, B. Konighofer, S. Pranger,
    in:, 31st International Conference on Computer-Aided Verification, Springer, 2019,
    pp. 630–649.
conference:
  end_date: 2019-07-18
  location: New York, NY, United States
  name: 'CAV: Computer Aided Verification'
  start_date: 2019-07-13
date_created: 2019-05-16T11:22:30Z
date_published: 2019-07-12T00:00:00Z
date_updated: 2023-08-25T10:33:27Z
day: '12'
ddc:
- '000'
department:
- _id: ToHe
- _id: KrCh
doi: 10.1007/978-3-030-25540-4_36
external_id:
  isi:
  - '000491468000036'
file:
- access_level: open_access
  checksum: c231579f2485c6fd4df17c9443a4d80b
  content_type: application/pdf
  creator: dernst
  date_created: 2019-08-14T09:35:24Z
  date_updated: 2020-07-14T12:47:31Z
  file_id: '6816'
  file_name: 2019_CAV_Avni.pdf
  file_size: 659766
  relation: main_file
file_date_updated: 2020-07-14T12:47:31Z
has_accepted_license: '1'
intvolume: '     11561'
isi: 1
language:
- iso: eng
month: '07'
oa: 1
oa_version: Published Version
page: 630-649
project:
- _id: 264B3912-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: M02369
  name: Formal Methods meets Algorithmic Game Theory
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
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: Run-time optimization for learned controllers through quantitative games
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: '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'
...