Membership-Based Synthesis of Linear Hybrid Automata

Cite This

Files in this item

Checksum: MD5:8e9bc4a5886fbae976ffc23b044c423e

GARCÍA SOTO, Miriam, Thomas A. HENZINGER, Christian SCHILLING, Luka ZELEZNIK, 2019. Membership-Based Synthesis of Linear Hybrid Automata. CAV 2019: Computer Aided Verification. New York, Jul 15, 2019 - Jul 18, 2019. In: DILLIG, Isil, ed., Serdar TASIRAN, ed.. Computer Aided Verification : 31st International Conference, CAV 2019, Proceedings, Part I. Cham:Springer International Publishing, pp. 297-314. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-030-25539-8. Available under: doi: 10.1007/978-3-030-25540-4_16

@inproceedings{GarciaSoto2019-07-12Membe-53574, title={Membership-Based Synthesis of Linear Hybrid Automata}, year={2019}, doi={10.1007/978-3-030-25540-4_16}, number={11561}, isbn={978-3-030-25539-8}, issn={0302-9743}, address={Cham}, publisher={Springer International Publishing}, series={Lecture Notes in Computer Science}, booktitle={Computer Aided Verification : 31st International Conference, CAV 2019, Proceedings, Part I}, pages={297--314}, editor={Dillig, Isil and Tasiran, Serdar}, author={García Soto, Miriam and Henzinger, Thomas A. and Schilling, Christian and Zeleznik, Luka} }

<rdf:RDF xmlns:dcterms="" xmlns:dc="" xmlns:rdf="" xmlns:bibo="" xmlns:dspace="" xmlns:foaf="" xmlns:void="" xmlns:xsd="" > <rdf:Description rdf:about=""> <dc:contributor>García Soto, Miriam</dc:contributor> <dc:creator>Zeleznik, Luka</dc:creator> <dcterms:abstract xml:lang="eng">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.</dcterms:abstract> <dc:creator>Henzinger, Thomas A.</dc:creator> <dcterms:isPartOf rdf:resource=""/> <dcterms:issued>2019-07-12</dcterms:issued> <dcterms:hasPart rdf:resource=""/> <dcterms:rights rdf:resource=""/> <bibo:uri rdf:resource=""/> <dc:date rdf:datatype="">2021-04-30T13:39:24Z</dc:date> <dc:language>eng</dc:language> <dc:rights>Attribution 4.0 International</dc:rights> <dcterms:title>Membership-Based Synthesis of Linear Hybrid Automata</dcterms:title> <dc:contributor>Zeleznik, Luka</dc:contributor> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dc:creator>Schilling, Christian</dc:creator> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dc:contributor>Henzinger, Thomas A.</dc:contributor> <dcterms:available rdf:datatype="">2021-04-30T13:39:24Z</dcterms:available> <dc:contributor>Schilling, Christian</dc:contributor> <dspace:isPartOfCollection rdf:resource=""/> <dc:creator>García Soto, Miriam</dc:creator> <dspace:hasBitstream rdf:resource=""/> </rdf:Description> </rdf:RDF>

Downloads since Apr 30, 2021 (Information about access statistics)

Garcia-Soto_2-whx4g6z9ce374.pdf 4

This item appears in the following Collection(s)

Attribution 4.0 International Except where otherwise noted, this item's license is described as Attribution 4.0 International

Search KOPS


My Account