---
res:
bibo_abstract:
- 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.@eng
bibo_authorlist:
- foaf_Person:
foaf_givenName: Miriam
foaf_name: Garcia Soto, Miriam
foaf_surname: Garcia Soto
foaf_workInfoHomepage: http://www.librecat.org/personId=4B3207F6-F248-11E8-B48F-1D18A9856A87
orcid: 0000−0003−2936−5719
- foaf_Person:
foaf_givenName: Thomas A
foaf_name: Henzinger, Thomas A
foaf_surname: Henzinger
foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
orcid: 0000−0002−2985−7724
- foaf_Person:
foaf_givenName: Christian
foaf_name: Schilling, Christian
foaf_surname: Schilling
foaf_workInfoHomepage: http://www.librecat.org/personId=3A2F4DCE-F248-11E8-B48F-1D18A9856A87
orcid: 0000-0003-3658-1065
- foaf_Person:
foaf_givenName: Luka
foaf_name: Zeleznik, Luka
foaf_surname: Zeleznik
foaf_workInfoHomepage: http://www.librecat.org/personId=3ADCA2E4-F248-11E8-B48F-1D18A9856A87
bibo_doi: 10.1007/978-3-030-25540-4_16
bibo_volume: 11561
dct_date: 2019^xs_gYear
dct_identifier:
- UT:000491468000016
dct_isPartOf:
- http://id.crossref.org/issn/0302-9743
- http://id.crossref.org/issn/9783030255398
dct_language: eng
dct_publisher: Springer@
dct_subject:
- Synthesis
- Linear hybrid automaton
- Membership
dct_title: Membership-based synthesis of linear hybrid automata@
...