Membership-based synthesis of linear hybrid automata

M. Garcia Soto, T.A. Henzinger, C. Schilling, L. Zeleznik, in:, 31st International Conference on Computer-Aided Verification, Springer, n.d.

Download
OA 469.62 KB
Conference Paper | Accepted | English
Department
Series Title
LNCS
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.
Publishing Year
Date Published
2019-01-01
Proceedings Title
31st International Conference on Computer-Aided Verification
Conference
CAV: Computer-Aided Verification
Conference Location
New York City, NY, USA
Conference Date
2019-07-15 – 2019-07-18
IST-REx-ID

Cite this

Garcia Soto M, Henzinger TA, Schilling C, Zeleznik L. Membership-based synthesis of linear hybrid automata. In: 31st International Conference on Computer-Aided Verification. Springer.
Garcia Soto, M., Henzinger, T. A., Schilling, C., & Zeleznik, L. (n.d.). Membership-based synthesis of linear hybrid automata. In 31st International Conference on Computer-Aided Verification. New York City, NY, USA: Springer.
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. Springer, n.d.
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.
Garcia Soto M, Henzinger TA, Schilling C, Zeleznik L. Membership-based synthesis of linear hybrid automata. 31st International Conference on Computer-Aided Verification. CAV: Computer-Aided Verification, LNCS,
Garcia Soto, Miriam, et al. “Membership-Based Synthesis of Linear Hybrid Automata.” 31st International Conference on Computer-Aided Verification, Springer.
Main File(s)
File Name
469.62 KB
Access Level
OA Open Access
Last Uploaded
2019-05-27T07:07:46Z


Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar