[{"page":"337-353","quality_controlled":"1","ec_funded":1,"publisher":"Springer Nature","_id":"12171","scopus_import":"1","author":[{"id":"4B3207F6-F248-11E8-B48F-1D18A9856A87","first_name":"Miriam","last_name":"Garcia Soto","orcid":"0000-0003-2936-5719","full_name":"Garcia Soto, Miriam"},{"full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Schilling, Christian","orcid":"0000-0003-3658-1065","last_name":"Schilling","first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87"}],"publication_status":"published","article_processing_charge":"No","date_created":"2023-01-12T12:11:16Z","department":[{"_id":"ToHe"}],"title":"Synthesis of parametric hybrid automata from time series","alternative_title":["LNCS"],"intvolume":"     13505","volume":13505,"acknowledgement":"This work was supported in part by the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement no. 847635, by the ERC-2020-AdG 101020093, by DIREC - Digital Research Centre Denmark, and by the Villum Investigator Grant S4OS.","date_updated":"2023-02-13T09:27:55Z","year":"2022","citation":{"apa":"Garcia Soto, M., Henzinger, T. A., &#38; Schilling, C. (2022). Synthesis of parametric hybrid automata from time series. In <i>20th International Symposium on Automated Technology for Verification and Analysis</i> (Vol. 13505, pp. 337–353). Virtual: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-19992-9_22\">https://doi.org/10.1007/978-3-031-19992-9_22</a>","ama":"Garcia Soto M, Henzinger TA, Schilling C. Synthesis of parametric hybrid automata from time series. In: <i>20th International Symposium on Automated Technology for Verification and Analysis</i>. Vol 13505. Springer Nature; 2022:337-353. doi:<a href=\"https://doi.org/10.1007/978-3-031-19992-9_22\">10.1007/978-3-031-19992-9_22</a>","ieee":"M. Garcia Soto, T. A. Henzinger, and C. Schilling, “Synthesis of parametric hybrid automata from time series,” in <i>20th International Symposium on Automated Technology for Verification and Analysis</i>, Virtual, 2022, vol. 13505, pp. 337–353.","chicago":"Garcia Soto, Miriam, Thomas A Henzinger, and Christian Schilling. “Synthesis of Parametric Hybrid Automata from Time Series.” In <i>20th International Symposium on Automated Technology for Verification and Analysis</i>, 13505:337–53. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-031-19992-9_22\">https://doi.org/10.1007/978-3-031-19992-9_22</a>.","short":"M. Garcia Soto, T.A. Henzinger, C. Schilling, in:, 20th International Symposium on Automated Technology for Verification and Analysis, Springer Nature, 2022, pp. 337–353.","mla":"Garcia Soto, Miriam, et al. “Synthesis of Parametric Hybrid Automata from Time Series.” <i>20th International Symposium on Automated Technology for Verification and Analysis</i>, vol. 13505, Springer Nature, 2022, pp. 337–53, doi:<a href=\"https://doi.org/10.1007/978-3-031-19992-9_22\">10.1007/978-3-031-19992-9_22</a>.","ista":"Garcia Soto M, Henzinger TA, Schilling C. 2022. Synthesis of parametric hybrid automata from time series. 20th International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 13505, 337–353."},"external_id":{"arxiv":["2208.06383"]},"arxiv":1,"doi":"10.1007/978-3-031-19992-9_22","day":"21","abstract":[{"lang":"eng","text":"We propose an algorithmic approach for synthesizing linear hybrid automata from time-series data. Unlike existing approaches, our approach provides a whole family of models with the same discrete structure but different dynamics. Each model in the family is guaranteed to capture the input data up to a precision error ε, in the following sense: For each time series, the model contains an execution that is ε-close to the data points. Our construction allows to effectively choose a model from this family with minimal precision error ε. We demonstrate the algorithm’s efficiency and its ability to find precise models in two case studies."}],"language":[{"iso":"eng"}],"conference":{"start_date":"2022-10-25","name":"ATVA: Automated Technology for Verification and Analysis","end_date":"2022-10-28","location":"Virtual"},"publication":"20th International Symposium on Automated Technology for Verification and Analysis","oa_version":"Preprint","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"month":"10","main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2208.06383","open_access":"1"}],"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_published":"2022-10-21T00:00:00Z","type":"conference","publication_identifier":{"eisbn":["9783031199929"],"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031199912"]},"oa":1},{"publisher":"Association for Computing Machinery","page":"2102.12734","quality_controlled":"1","ec_funded":1,"file_date_updated":"2021-05-25T13:53:22Z","publication_status":"published","department":[{"_id":"ToHe"}],"article_processing_charge":"No","date_created":"2021-02-26T16:30:39Z","title":"Synthesis of hybrid automata with affine dynamics from time-series data","_id":"9200","scopus_import":"1","author":[{"id":"4B3207F6-F248-11E8-B48F-1D18A9856A87","last_name":"Garcia Soto","first_name":"Miriam","full_name":"Garcia Soto, Miriam","orcid":"0000-0003-2936-5719"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger"},{"first_name":"Christian","last_name":"Schilling","orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87"}],"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.","ddc":["000"],"arxiv":1,"doi":"10.1145/3447928.3456704","day":"01","abstract":[{"lang":"eng","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."}],"date_updated":"2023-08-07T13:49:33Z","citation":{"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.” <i>HSCC ’21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control</i>, Association for Computing Machinery, 2021, p. 2102.12734, doi:<a href=\"https://doi.org/10.1145/3447928.3456704\">10.1145/3447928.3456704</a>.","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.","ama":"Garcia Soto M, Henzinger TA, Schilling C. Synthesis of hybrid automata with affine dynamics from time-series data. In: <i>HSCC ’21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control</i>. Association for Computing Machinery; 2021:2102.12734. doi:<a href=\"https://doi.org/10.1145/3447928.3456704\">10.1145/3447928.3456704</a>","apa":"Garcia Soto, M., Henzinger, T. A., &#38; Schilling, C. (2021). Synthesis of hybrid automata with affine dynamics from time-series data. In <i>HSCC ’21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control</i> (p. 2102.12734). Nashville, TN, United States: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3447928.3456704\">https://doi.org/10.1145/3447928.3456704</a>","ieee":"M. Garcia Soto, T. A. Henzinger, and C. Schilling, “Synthesis of hybrid automata with affine dynamics from time-series data,” in <i>HSCC ’21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control</i>, Nashville, TN, United States, 2021, p. 2102.12734.","chicago":"Garcia Soto, Miriam, Thomas A Henzinger, and Christian Schilling. “Synthesis of Hybrid Automata with Affine Dynamics from Time-Series Data.” In <i>HSCC ’21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control</i>, 2102.12734. Association for Computing Machinery, 2021. <a href=\"https://doi.org/10.1145/3447928.3456704\">https://doi.org/10.1145/3447928.3456704</a>."},"year":"2021","isi":1,"external_id":{"isi":["000932821700028"],"arxiv":["2102.12734"]},"conference":{"end_date":"2021-05-21","location":"Nashville, TN, United States","name":"HSCC: International Conference on Hybrid Systems Computation and Control","start_date":"2021-05-19"},"language":[{"iso":"eng"}],"keyword":["hybrid automaton","membership","system identification"],"oa_version":"Published Version","project":[{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships","call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425"}],"month":"05","publication":"HSCC '21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control","has_accepted_license":"1","file":[{"relation":"main_file","success":1,"access_level":"open_access","creator":"kschuh","file_id":"9424","file_size":1474786,"checksum":"4c1202c1abf71384c3ee6fea88c2f80e","date_created":"2021-05-25T13:53:22Z","content_type":"application/pdf","file_name":"2021_HSCC_Soto.pdf","date_updated":"2021-05-25T13:53:22Z"}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","status":"public","publication_identifier":{"isbn":["9781450383394"]},"oa":1,"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"date_published":"2021-05-01T00:00:00Z","type":"conference"},{"ddc":["000"],"volume":36,"abstract":[{"text":"This paper presents a novel abstraction technique for analyzing Lyapunov and asymptotic stability of polyhedral switched systems. A polyhedral switched system is a hybrid system in which the continuous dynamics is specified by polyhedral differential inclusions, the invariants and guards are specified by polyhedral sets and the switching between the modes do not involve reset of variables. A finite state weighted graph abstracting the polyhedral switched system is constructed from a finite partition of the state–space, such that the satisfaction of certain graph conditions, such as the absence of cycles with product of weights on the edges greater than (or equal) to 1, implies the stability of the system. However, the graph is in general conservative and hence, the violation of the graph conditions does not imply instability. If the analysis fails to establish stability due to the conservativeness in the approximation, a counterexample (cycle with product of edge weights greater than or equal to 1) indicating a potential reason for the failure is returned. Further, a more precise approximation of the switched system can be constructed by considering a finer partition of the state–space in the construction of the finite weighted graph. We present experimental results on analyzing stability of switched systems using the above method.","lang":"eng"}],"doi":"10.1016/j.nahs.2020.100856","day":"01","isi":1,"external_id":{"isi":["000528828600003"]},"date_updated":"2023-08-17T14:32:54Z","citation":{"ista":"Garcia Soto M, Prabhakar P. 2020. Abstraction based verification of stability of polyhedral switched systems. Nonlinear Analysis: Hybrid Systems. 36(5), 100856.","short":"M. Garcia Soto, P. Prabhakar, Nonlinear Analysis: Hybrid Systems 36 (2020).","mla":"Garcia Soto, Miriam, and Pavithra Prabhakar. “Abstraction Based Verification of Stability of Polyhedral Switched Systems.” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 36, no. 5, 100856, Elsevier, 2020, doi:<a href=\"https://doi.org/10.1016/j.nahs.2020.100856\">10.1016/j.nahs.2020.100856</a>.","ieee":"M. Garcia Soto and P. Prabhakar, “Abstraction based verification of stability of polyhedral switched systems,” <i>Nonlinear Analysis: Hybrid Systems</i>, vol. 36, no. 5. Elsevier, 2020.","chicago":"Garcia Soto, Miriam, and Pavithra Prabhakar. “Abstraction Based Verification of Stability of Polyhedral Switched Systems.” <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier, 2020. <a href=\"https://doi.org/10.1016/j.nahs.2020.100856\">https://doi.org/10.1016/j.nahs.2020.100856</a>.","ama":"Garcia Soto M, Prabhakar P. Abstraction based verification of stability of polyhedral switched systems. <i>Nonlinear Analysis: Hybrid Systems</i>. 2020;36(5). doi:<a href=\"https://doi.org/10.1016/j.nahs.2020.100856\">10.1016/j.nahs.2020.100856</a>","apa":"Garcia Soto, M., &#38; Prabhakar, P. (2020). Abstraction based verification of stability of polyhedral switched systems. <i>Nonlinear Analysis: Hybrid Systems</i>. Elsevier. <a href=\"https://doi.org/10.1016/j.nahs.2020.100856\">https://doi.org/10.1016/j.nahs.2020.100856</a>"},"year":"2020","article_type":"original","publisher":"Elsevier","file_date_updated":"2022-05-16T22:30:04Z","quality_controlled":"1","title":"Abstraction based verification of stability of polyhedral switched systems","intvolume":"        36","publication_status":"published","date_created":"2020-02-02T23:00:59Z","department":[{"_id":"ToHe"}],"article_processing_charge":"No","author":[{"full_name":"Garcia Soto, Miriam","orcid":"0000−0003−2936−5719","last_name":"Garcia Soto","first_name":"Miriam","id":"4B3207F6-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Prabhakar, Pavithra","last_name":"Prabhakar","first_name":"Pavithra"}],"issue":"5","_id":"7426","scopus_import":"1","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","status":"public","file":[{"file_id":"8688","creator":"dernst","access_level":"open_access","relation":"main_file","date_updated":"2022-05-16T22:30:04Z","file_name":"2020_NAHS_GarciaSoto.pdf","content_type":"application/pdf","date_created":"2020-10-21T13:16:45Z","embargo":"2022-05-15","file_size":818774,"checksum":"560abfddb53f9fe921b6744f59f2cfaa"}],"oa":1,"publication_identifier":{"issn":["1751-570X"]},"date_published":"2020-05-01T00:00:00Z","type":"journal_article","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","short":"CC BY-NC-ND (4.0)","name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","image":"/images/cc_by_nc_nd.png"},"language":[{"iso":"eng"}],"month":"05","article_number":"100856","oa_version":"Submitted Version","project":[{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11407","name":"Game Theory"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"}],"publication":"Nonlinear Analysis: Hybrid Systems","has_accepted_license":"1"},{"file_date_updated":"2021-02-26T16:38:14Z","page":"244-256","quality_controlled":"1","publisher":"IEEE","author":[{"full_name":"Garcia Soto, Miriam","orcid":"0000-0003-2936-5719","last_name":"Garcia Soto","first_name":"Miriam","id":"4B3207F6-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Pavithra","last_name":"Prabhakar","full_name":"Prabhakar, Pavithra"}],"_id":"9202","title":"Hybridization for stability verification of nonlinear switched systems","publication_status":"published","article_processing_charge":"No","date_created":"2021-02-26T16:38:24Z","department":[{"_id":"ToHe"}],"ddc":["000"],"acknowledgement":"Miriam Garc´ıa Soto was partially supported by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award). Pavithra Prabhakar was partially supported by NSF CAREER Award No. 1552668, NSF Award No. 2008957 and ONR YIP Award No. N000141712577.","isi":1,"external_id":{"isi":["000680435100021"]},"date_updated":"2024-02-22T13:25:19Z","year":"2020","citation":{"mla":"Garcia Soto, Miriam, and Pavithra Prabhakar. “Hybridization for Stability Verification of Nonlinear Switched Systems.” <i>2020 IEEE Real-Time Systems Symposium</i>, IEEE, 2020, pp. 244–56, doi:<a href=\"https://doi.org/10.1109/RTSS49844.2020.00031\">10.1109/RTSS49844.2020.00031</a>.","short":"M. Garcia Soto, P. Prabhakar, in:, 2020 IEEE Real-Time Systems Symposium, IEEE, 2020, pp. 244–256.","ista":"Garcia Soto M, Prabhakar P. 2020. Hybridization for stability verification of nonlinear switched systems. 2020 IEEE Real-Time Systems Symposium. RTTS: Real-Time Systems Symposium, 244–256.","apa":"Garcia Soto, M., &#38; Prabhakar, P. (2020). Hybridization for stability verification of nonlinear switched systems. In <i>2020 IEEE Real-Time Systems Symposium</i> (pp. 244–256). Houston, TX, USA : IEEE. <a href=\"https://doi.org/10.1109/RTSS49844.2020.00031\">https://doi.org/10.1109/RTSS49844.2020.00031</a>","ama":"Garcia Soto M, Prabhakar P. Hybridization for stability verification of nonlinear switched systems. In: <i>2020 IEEE Real-Time Systems Symposium</i>. IEEE; 2020:244-256. doi:<a href=\"https://doi.org/10.1109/RTSS49844.2020.00031\">10.1109/RTSS49844.2020.00031</a>","ieee":"M. Garcia Soto and P. Prabhakar, “Hybridization for stability verification of nonlinear switched systems,” in <i>2020 IEEE Real-Time Systems Symposium</i>, Houston, TX, USA , 2020, pp. 244–256.","chicago":"Garcia Soto, Miriam, and Pavithra Prabhakar. “Hybridization for Stability Verification of Nonlinear Switched Systems.” In <i>2020 IEEE Real-Time Systems Symposium</i>, 244–56. IEEE, 2020. <a href=\"https://doi.org/10.1109/RTSS49844.2020.00031\">https://doi.org/10.1109/RTSS49844.2020.00031</a>."},"abstract":[{"lang":"eng","text":"We propose a novel hybridization method for stability analysis that over-approximates nonlinear dynamical systems by switched systems with linear inclusion dynamics. We observe that existing hybridization techniques for safety analysis that over-approximate nonlinear dynamical systems by switched affine inclusion dynamics and provide fixed approximation error, do not suffice for stability analysis. Hence, we propose a hybridization method that provides a state-dependent error which converges to zero as the state tends to the equilibrium point. The crux of our hybridization computation is an elegant recursive algorithm that uses partial derivatives of a given function to obtain upper and lower bound matrices for the over-approximating linear inclusion. We illustrate our method on some examples to demonstrate the application of the theory for stability analysis. In particular, our method is able to establish stability of a nonlinear system which does not admit a polynomial Lyapunov function."}],"doi":"10.1109/RTSS49844.2020.00031","day":"01","language":[{"iso":"eng"}],"conference":{"location":"Houston, TX, USA ","end_date":"2020-12-04","name":"RTTS: Real-Time Systems Symposium","start_date":"2020-12-01"},"publication":"2020 IEEE Real-Time Systems Symposium","has_accepted_license":"1","month":"12","oa_version":"Submitted Version","project":[{"name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","status":"public","file":[{"creator":"mgarcias","file_id":"9203","relation":"main_file","access_level":"open_access","file_name":"main.pdf","content_type":"application/pdf","date_updated":"2021-02-26T16:38:14Z","file_size":1125794,"checksum":"8f97f229316c3b3a6f0cf99297aa0941","date_created":"2021-02-26T16:38:14Z"}],"date_published":"2020-12-01T00:00:00Z","type":"conference","oa":1,"publication_identifier":{"eissn":["2576-3172"],"eisbn":["9781728183244"]}},{"_id":"6493","scopus_import":"1","author":[{"first_name":"Miriam","last_name":"Garcia Soto","orcid":"0000−0003−2936−5719","full_name":"Garcia Soto, Miriam","id":"4B3207F6-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","first_name":"Christian","last_name":"Schilling","orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian"},{"id":"3ADCA2E4-F248-11E8-B48F-1D18A9856A87","first_name":"Luka","last_name":"Zeleznik","full_name":"Zeleznik, Luka"}],"publication_status":"published","department":[{"_id":"ToHe"}],"article_processing_charge":"No","date_created":"2019-05-27T07:09:53Z","alternative_title":["LNCS"],"title":"Membership-based synthesis of linear hybrid automata","intvolume":"     11561","page":"297-314","ec_funded":1,"quality_controlled":"1","file_date_updated":"2020-07-14T12:47:32Z","publisher":"Springer","date_updated":"2023-08-25T10:40:41Z","citation":{"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.” <i>31st International Conference on Computer-Aided Verification</i>, vol. 11561, Springer, 2019, pp. 297–314, doi:<a href=\"https://doi.org/10.1007/978-3-030-25540-4_16\">10.1007/978-3-030-25540-4_16</a>.","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.","apa":"Garcia Soto, M., Henzinger, T. A., Schilling, C., &#38; Zeleznik, L. (2019). Membership-based synthesis of linear hybrid automata. In <i>31st International Conference on Computer-Aided Verification</i> (Vol. 11561, pp. 297–314). New York City, NY, USA: Springer. <a href=\"https://doi.org/10.1007/978-3-030-25540-4_16\">https://doi.org/10.1007/978-3-030-25540-4_16</a>","ama":"Garcia Soto M, Henzinger TA, Schilling C, Zeleznik L. Membership-based synthesis of linear hybrid automata. In: <i>31st International Conference on Computer-Aided Verification</i>. Vol 11561. Springer; 2019:297-314. doi:<a href=\"https://doi.org/10.1007/978-3-030-25540-4_16\">10.1007/978-3-030-25540-4_16</a>","ieee":"M. Garcia Soto, T. A. Henzinger, C. Schilling, and L. Zeleznik, “Membership-based synthesis of linear hybrid automata,” in <i>31st International Conference on Computer-Aided Verification</i>, New York City, NY, USA, 2019, vol. 11561, pp. 297–314.","chicago":"Garcia Soto, Miriam, Thomas A Henzinger, Christian Schilling, and Luka Zeleznik. “Membership-Based Synthesis of Linear Hybrid Automata.” In <i>31st International Conference on Computer-Aided Verification</i>, 11561:297–314. Springer, 2019. <a href=\"https://doi.org/10.1007/978-3-030-25540-4_16\">https://doi.org/10.1007/978-3-030-25540-4_16</a>."},"year":"2019","isi":1,"external_id":{"isi":["000491468000016"]},"doi":"10.1007/978-3-030-25540-4_16","day":"12","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."}],"volume":11561,"ddc":["000"],"publication":"31st International Conference on Computer-Aided Verification","has_accepted_license":"1","oa_version":"Published Version","project":[{"grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships","call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"}],"month":"07","language":[{"iso":"eng"}],"keyword":["Synthesis","Linear hybrid automaton","Membership"],"conference":{"end_date":"2019-07-18","location":"New York City, NY, USA","start_date":"2019-07-15","name":"CAV: Computer-Aided Verification"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"date_published":"2019-07-12T00:00:00Z","type":"conference","publication_identifier":{"issn":["0302-9743"],"isbn":["9783030255398"]},"oa":1,"file":[{"file_id":"6817","creator":"dernst","relation":"main_file","access_level":"open_access","date_updated":"2020-07-14T12:47:32Z","content_type":"application/pdf","file_name":"2019_CAV_GarciaSoto.pdf","date_created":"2019-08-14T11:05:30Z","checksum":"1f1d61b83a151031745ef70a501da3d6","file_size":674795}],"status":"public","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8"},{"language":[{"iso":"eng"}],"conference":{"end_date":"2019-01-11","location":"Delhi, India","start_date":"2019-01-09","name":"ICC 2019 - Indian Control Conference"},"publication":"5th Indian Control Conference Proceedings","has_accepted_license":"1","month":"05","article_number":"8715598","oa_version":"Submitted Version","project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"}],"status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","file":[{"success":1,"relation":"main_file","access_level":"open_access","file_id":"8687","creator":"dernst","date_created":"2020-10-21T13:13:49Z","checksum":"d622a91af1e427f6b1e0ba8e18a2b767","file_size":396031,"date_updated":"2020-10-21T13:13:49Z","file_name":"2019_ICC_Kundu.pdf","content_type":"application/pdf"}],"date_published":"2019-05-16T00:00:00Z","type":"conference","oa":1,"publication_identifier":{"isbn":["978-153866246-5"]},"file_date_updated":"2020-10-21T13:13:49Z","quality_controlled":"1","publisher":"IEEE","author":[{"full_name":"Kundu, Atreyee","first_name":"Atreyee","last_name":"Kundu"},{"id":"4B3207F6-F248-11E8-B48F-1D18A9856A87","full_name":"Garcia Soto, Miriam","orcid":"0000−0003−2936−5719","last_name":"Garcia Soto","first_name":"Miriam"},{"full_name":"Prabhakar, Pavithra","last_name":"Prabhakar","first_name":"Pavithra"}],"_id":"6565","scopus_import":"1","title":"Formal synthesis of stabilizing controllers for periodically controlled linear switched systems","publication_status":"published","department":[{"_id":"ToHe"}],"date_created":"2019-06-17T06:57:33Z","article_processing_charge":"No","ddc":["000"],"date_updated":"2021-01-12T08:08:01Z","citation":{"ieee":"A. Kundu, M. Garcia Soto, and P. Prabhakar, “Formal synthesis of stabilizing controllers for periodically controlled linear switched systems,” in <i>5th Indian Control Conference Proceedings</i>, Delhi, India, 2019.","chicago":"Kundu, Atreyee, Miriam Garcia Soto, and Pavithra Prabhakar. “Formal Synthesis of Stabilizing Controllers for Periodically Controlled Linear Switched Systems.” In <i>5th Indian Control Conference Proceedings</i>. IEEE, 2019. <a href=\"https://doi.org/10.1109/INDIANCC.2019.8715598\">https://doi.org/10.1109/INDIANCC.2019.8715598</a>.","apa":"Kundu, A., Garcia Soto, M., &#38; Prabhakar, P. (2019). Formal synthesis of stabilizing controllers for periodically controlled linear switched systems. In <i>5th Indian Control Conference Proceedings</i>. Delhi, India: IEEE. <a href=\"https://doi.org/10.1109/INDIANCC.2019.8715598\">https://doi.org/10.1109/INDIANCC.2019.8715598</a>","ama":"Kundu A, Garcia Soto M, Prabhakar P. Formal synthesis of stabilizing controllers for periodically controlled linear switched systems. In: <i>5th Indian Control Conference Proceedings</i>. IEEE; 2019. doi:<a href=\"https://doi.org/10.1109/INDIANCC.2019.8715598\">10.1109/INDIANCC.2019.8715598</a>","ista":"Kundu A, Garcia Soto M, Prabhakar P. 2019. Formal synthesis of stabilizing controllers for periodically controlled linear switched systems. 5th Indian Control Conference Proceedings. ICC 2019 - Indian Control Conference, 8715598.","mla":"Kundu, Atreyee, et al. “Formal Synthesis of Stabilizing Controllers for Periodically Controlled Linear Switched Systems.” <i>5th Indian Control Conference Proceedings</i>, 8715598, IEEE, 2019, doi:<a href=\"https://doi.org/10.1109/INDIANCC.2019.8715598\">10.1109/INDIANCC.2019.8715598</a>.","short":"A. Kundu, M. Garcia Soto, P. Prabhakar, in:, 5th Indian Control Conference Proceedings, IEEE, 2019."},"year":"2019","abstract":[{"lang":"eng","text":"In this paper, we address the problem of synthesizing periodic switching controllers for stabilizing a family of linear systems. Our broad approach consists of constructing a finite game graph based on the family of linear systems such that every winning strategy on the game graph corresponds to a stabilizing switching controller for the family of linear systems. The construction of a (finite) game graph, the synthesis of a winning strategy and the extraction of a stabilizing controller are all computationally feasible. We illustrate our method on an example."}],"doi":"10.1109/INDIANCC.2019.8715598","day":"16"}]