---
_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: 31st International Conference on Computer-Aided
Verification. Vol 11561. Springer; 2019:297-314. doi:10.1007/978-3-030-25540-4_16'
apa: 'Garcia Soto, M., Henzinger, T. A., Schilling, C., & Zeleznik, L. (2019).
Membership-based synthesis of linear hybrid automata. In 31st International
Conference on Computer-Aided Verification (Vol. 11561, pp. 297–314). New York
City, NY, USA: Springer. https://doi.org/10.1007/978-3-030-25540-4_16'
chicago: Garcia Soto, Miriam, Thomas A Henzinger, Christian Schilling, and Luka
Zeleznik. “Membership-Based Synthesis of Linear Hybrid Automata.” In 31st International
Conference on Computer-Aided Verification, 11561:297–314. Springer, 2019.
https://doi.org/10.1007/978-3-030-25540-4_16.
ieee: M. Garcia Soto, T. A. Henzinger, C. Schilling, and L. Zeleznik, “Membership-based
synthesis of linear hybrid automata,” in 31st International Conference on Computer-Aided
Verification, 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.”
31st International Conference on Computer-Aided Verification, vol. 11561,
Springer, 2019, pp. 297–314, doi:10.1007/978-3-030-25540-4_16.
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'
...