[{"file":[{"relation":"main_file","file_id":"9424","date_updated":"2021-05-25T13:53:22Z","date_created":"2021-05-25T13:53:22Z","checksum":"4c1202c1abf71384c3ee6fea88c2f80e","success":1,"file_name":"2021_HSCC_Soto.pdf","access_level":"open_access","content_type":"application/pdf","file_size":1474786,"creator":"kschuh"}],"oa_version":"Published Version","title":"Synthesis of hybrid automata with affine dynamics from time-series data","ddc":["000"],"status":"public","_id":"9200","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","abstract":[{"text":"Formal design of embedded and cyber-physical systems relies on mathematical modeling. In this paper, we consider the model class of hybrid automata whose dynamics are defined by affine differential equations. Given a set of time-series data, we present an algorithmic approach to synthesize a hybrid automaton exhibiting behavior that is close to the data, up to a specified precision, and changes in synchrony with the data. A fundamental problem in our synthesis algorithm is to check membership of a time series in a hybrid automaton. Our solution integrates reachability and optimization techniques for affine dynamical systems to obtain both a sufficient and a necessary condition for membership, combined in a refinement framework. The algorithm processes one time series at a time and hence can be interrupted, provide an intermediate result, and be resumed. We report experimental results demonstrating the applicability of our synthesis approach.","lang":"eng"}],"type":"conference","date_published":"2021-05-01T00:00:00Z","page":"2102.12734","publication":"HSCC '21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control","citation":{"ama":"Garcia Soto M, Henzinger TA, Schilling C. Synthesis of hybrid automata with affine dynamics from time-series data. In: HSCC ’21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control. Association for Computing Machinery; 2021:2102.12734. doi:10.1145/3447928.3456704","apa":"Garcia Soto, M., Henzinger, T. A., & Schilling, C. (2021). Synthesis of hybrid automata with affine dynamics from time-series data. In HSCC ’21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control (p. 2102.12734). Nashville, TN, United States: Association for Computing Machinery. https://doi.org/10.1145/3447928.3456704","ieee":"M. Garcia Soto, T. A. Henzinger, and C. Schilling, “Synthesis of hybrid automata with affine dynamics from time-series data,” in HSCC ’21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control, Nashville, TN, United States, 2021, p. 2102.12734.","ista":"Garcia Soto M, Henzinger TA, Schilling C. 2021. Synthesis of hybrid automata with affine dynamics from time-series data. HSCC ’21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control. HSCC: International Conference on Hybrid Systems Computation and Control, 2102.12734.","short":"M. Garcia Soto, T.A. Henzinger, C. Schilling, in:, HSCC ’21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control, Association for Computing Machinery, 2021, p. 2102.12734.","mla":"Garcia Soto, Miriam, et al. “Synthesis of Hybrid Automata with Affine Dynamics from Time-Series Data.” HSCC ’21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control, Association for Computing Machinery, 2021, p. 2102.12734, doi:10.1145/3447928.3456704.","chicago":"Garcia Soto, Miriam, Thomas A Henzinger, and Christian Schilling. “Synthesis of Hybrid Automata with Affine Dynamics from Time-Series Data.” In HSCC ’21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control, 2102.12734. Association for Computing Machinery, 2021. https://doi.org/10.1145/3447928.3456704."},"day":"01","has_accepted_license":"1","article_processing_charge":"No","keyword":["hybrid automaton","membership","system identification"],"scopus_import":"1","date_created":"2021-02-26T16:30:39Z","date_updated":"2023-08-07T13:49:33Z","author":[{"last_name":"Garcia Soto","first_name":"Miriam","orcid":"0000-0003-2936-5719","id":"4B3207F6-F248-11E8-B48F-1D18A9856A87","full_name":"Garcia Soto, Miriam"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"first_name":"Christian","last_name":"Schilling","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian"}],"publication_status":"published","publisher":"Association for Computing Machinery","department":[{"_id":"ToHe"}],"year":"2021","acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award) and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No. 754411.","file_date_updated":"2021-05-25T13:53:22Z","ec_funded":1,"language":[{"iso":"eng"}],"conference":{"end_date":"2021-05-21","location":"Nashville, TN, United States","start_date":"2021-05-19","name":"HSCC: International Conference on Hybrid Systems Computation and Control"},"doi":"10.1145/3447928.3456704","isi":1,"quality_controlled":"1","project":[{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","call_identifier":"FWF","name":"The Wittgenstein Prize"},{"name":"ISTplus - Postdoctoral Fellowships","call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425","grant_number":"754411"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"external_id":{"arxiv":["2102.12734"],"isi":["000932821700028"]},"oa":1,"month":"05","publication_identifier":{"isbn":["9781450383394"]}},{"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"],"type":"conference","file":[{"checksum":"1f1d61b83a151031745ef70a501da3d6","date_updated":"2020-07-14T12:47:32Z","date_created":"2019-08-14T11:05:30Z","relation":"main_file","file_id":"6817","file_size":674795,"content_type":"application/pdf","creator":"dernst","access_level":"open_access","file_name":"2019_CAV_GarciaSoto.pdf"}],"oa_version":"Published Version","ddc":["000"],"title":"Membership-based synthesis of linear hybrid automata","status":"public","intvolume":" 11561","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","_id":"6493","day":"12","article_processing_charge":"No","has_accepted_license":"1","keyword":["Synthesis","Linear hybrid automaton","Membership"],"scopus_import":"1","date_published":"2019-07-12T00:00:00Z","page":"297-314","publication":"31st International Conference on Computer-Aided Verification","citation":{"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.","short":"M. Garcia Soto, T.A. Henzinger, C. Schilling, L. Zeleznik, in:, 31st International Conference on Computer-Aided Verification, Springer, 2019, pp. 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.","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","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.","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"},"file_date_updated":"2020-07-14T12:47:32Z","ec_funded":1,"date_created":"2019-05-27T07:09:53Z","date_updated":"2023-08-25T10:40:41Z","volume":11561,"author":[{"last_name":"Garcia Soto","first_name":"Miriam","orcid":"0000−0003−2936−5719","id":"4B3207F6-F248-11E8-B48F-1D18A9856A87","full_name":"Garcia Soto, Miriam"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"},{"id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-3658-1065","first_name":"Christian","last_name":"Schilling","full_name":"Schilling, Christian"},{"id":"3ADCA2E4-F248-11E8-B48F-1D18A9856A87","last_name":"Zeleznik","first_name":"Luka","full_name":"Zeleznik, Luka"}],"publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"Springer","year":"2019","month":"07","publication_identifier":{"isbn":["9783030255398"],"issn":["0302-9743"]},"language":[{"iso":"eng"}],"conference":{"location":"New York City, NY, USA","start_date":"2019-07-15","end_date":"2019-07-18","name":"CAV: Computer-Aided Verification"},"doi":"10.1007/978-3-030-25540-4_16","quality_controlled":"1","isi":1,"project":[{"grant_number":"754411","_id":"260C2330-B435-11E9-9278-68D0E5697425","name":"ISTplus - Postdoctoral Fellowships","call_identifier":"H2020"},{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"external_id":{"isi":["000491468000016"]},"oa":1}]