[{"quality_controlled":"1","project":[{"grant_number":"101020093","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software"}],"oa":1,"external_id":{"arxiv":["2208.06383"]},"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2208.06383"}],"language":[{"iso":"eng"}],"conference":{"name":"ATVA: Automated Technology for Verification and Analysis","location":"Virtual","start_date":"2022-10-25","end_date":"2022-10-28"},"doi":"10.1007/978-3-031-19992-9_22","month":"10","publication_identifier":{"eisbn":["9783031199929"],"issn":["0302-9743"],"isbn":["9783031199912"],"eissn":["1611-3349"]},"publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"Springer Nature","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.","year":"2022","date_updated":"2023-02-13T09:27:55Z","date_created":"2023-01-12T12:11:16Z","volume":13505,"author":[{"full_name":"Garcia Soto, Miriam","first_name":"Miriam","last_name":"Garcia Soto","id":"4B3207F6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-2936-5719"},{"orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A","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"}],"ec_funded":1,"page":"337-353","publication":"20th International Symposium on Automated Technology for Verification and Analysis","citation":{"ieee":"M. Garcia Soto, T. A. Henzinger, and C. Schilling, “Synthesis of parametric hybrid automata from time series,” in 20th International Symposium on Automated Technology for Verification and Analysis, Virtual, 2022, vol. 13505, pp. 337–353.","apa":"Garcia Soto, M., Henzinger, T. A., & Schilling, C. (2022). Synthesis of parametric hybrid automata from time series. In 20th International Symposium on Automated Technology for Verification and Analysis (Vol. 13505, pp. 337–353). Virtual: Springer Nature. https://doi.org/10.1007/978-3-031-19992-9_22","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.","ama":"Garcia Soto M, Henzinger TA, Schilling C. Synthesis of parametric hybrid automata from time series. In: 20th International Symposium on Automated Technology for Verification and Analysis. Vol 13505. Springer Nature; 2022:337-353. doi:10.1007/978-3-031-19992-9_22","chicago":"Garcia Soto, Miriam, Thomas A Henzinger, and Christian Schilling. “Synthesis of Parametric Hybrid Automata from Time Series.” In 20th International Symposium on Automated Technology for Verification and Analysis, 13505:337–53. Springer Nature, 2022. https://doi.org/10.1007/978-3-031-19992-9_22.","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.” 20th International Symposium on Automated Technology for Verification and Analysis, vol. 13505, Springer Nature, 2022, pp. 337–53, doi:10.1007/978-3-031-19992-9_22."},"date_published":"2022-10-21T00:00:00Z","scopus_import":"1","day":"21","article_processing_charge":"No","title":"Synthesis of parametric hybrid automata from time series","status":"public","intvolume":" 13505","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"12171","oa_version":"Preprint","alternative_title":["LNCS"],"type":"conference","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."}]},{"type":"conference","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"}],"_id":"9200","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","status":"public","ddc":["000"],"title":"Synthesis of hybrid automata with affine dynamics from time-series data","file":[{"access_level":"open_access","file_name":"2021_HSCC_Soto.pdf","creator":"kschuh","file_size":1474786,"content_type":"application/pdf","file_id":"9424","relation":"main_file","success":1,"checksum":"4c1202c1abf71384c3ee6fea88c2f80e","date_created":"2021-05-25T13:53:22Z","date_updated":"2021-05-25T13:53:22Z"}],"oa_version":"Published Version","scopus_import":"1","keyword":["hybrid automaton","membership","system identification"],"has_accepted_license":"1","article_processing_charge":"No","day":"01","citation":{"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.","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.","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.","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","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.","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.","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"},"publication":"HSCC '21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control","page":"2102.12734","date_published":"2021-05-01T00:00:00Z","ec_funded":1,"file_date_updated":"2021-05-25T13:53:22Z","license":"https://creativecommons.org/licenses/by/4.0/","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.","department":[{"_id":"ToHe"}],"publisher":"Association for Computing Machinery","publication_status":"published","author":[{"last_name":"Garcia Soto","first_name":"Miriam","orcid":"0000-0003-2936-5719","id":"4B3207F6-F248-11E8-B48F-1D18A9856A87","full_name":"Garcia Soto, Miriam"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","first_name":"Thomas A","last_name":"Henzinger","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"}],"date_created":"2021-02-26T16:30:39Z","date_updated":"2023-08-07T13:49:33Z","publication_identifier":{"isbn":["9781450383394"]},"month":"05","oa":1,"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":["000932821700028"],"arxiv":["2102.12734"]},"project":[{"call_identifier":"FWF","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"},{"name":"ISTplus - Postdoctoral Fellowships","call_identifier":"H2020","grant_number":"754411","_id":"260C2330-B435-11E9-9278-68D0E5697425"}],"isi":1,"quality_controlled":"1","doi":"10.1145/3447928.3456704","conference":{"name":"HSCC: International Conference on Hybrid Systems Computation and Control","end_date":"2021-05-21","location":"Nashville, TN, United States","start_date":"2021-05-19"},"language":[{"iso":"eng"}]},{"project":[{"call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425"}],"isi":1,"quality_controlled":"1","external_id":{"isi":["000680435100021"]},"oa":1,"language":[{"iso":"eng"}],"doi":"10.1109/RTSS49844.2020.00031","conference":{"start_date":"2020-12-01","location":"Houston, TX, USA ","end_date":"2020-12-04","name":"RTTS: Real-Time Systems Symposium"},"publication_identifier":{"eisbn":["9781728183244"],"eissn":["2576-3172"]},"month":"12","publisher":"IEEE","department":[{"_id":"ToHe"}],"publication_status":"published","year":"2020","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.","date_created":"2021-02-26T16:38:24Z","date_updated":"2024-02-22T13:25:19Z","author":[{"id":"4B3207F6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-2936-5719","first_name":"Miriam","last_name":"Garcia Soto","full_name":"Garcia Soto, Miriam"},{"full_name":"Prabhakar, Pavithra","last_name":"Prabhakar","first_name":"Pavithra"}],"file_date_updated":"2021-02-26T16:38:14Z","page":"244-256","citation":{"ama":"Garcia Soto M, Prabhakar P. Hybridization for stability verification of nonlinear switched systems. In: 2020 IEEE Real-Time Systems Symposium. IEEE; 2020:244-256. doi:10.1109/RTSS49844.2020.00031","ieee":"M. Garcia Soto and P. Prabhakar, “Hybridization for stability verification of nonlinear switched systems,” in 2020 IEEE Real-Time Systems Symposium, Houston, TX, USA , 2020, pp. 244–256.","apa":"Garcia Soto, M., & Prabhakar, P. (2020). Hybridization for stability verification of nonlinear switched systems. In 2020 IEEE Real-Time Systems Symposium (pp. 244–256). Houston, TX, USA : IEEE. https://doi.org/10.1109/RTSS49844.2020.00031","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.","short":"M. Garcia Soto, P. Prabhakar, in:, 2020 IEEE Real-Time Systems Symposium, IEEE, 2020, pp. 244–256.","mla":"Garcia Soto, Miriam, and Pavithra Prabhakar. “Hybridization for Stability Verification of Nonlinear Switched Systems.” 2020 IEEE Real-Time Systems Symposium, IEEE, 2020, pp. 244–56, doi:10.1109/RTSS49844.2020.00031.","chicago":"Garcia Soto, Miriam, and Pavithra Prabhakar. “Hybridization for Stability Verification of Nonlinear Switched Systems.” In 2020 IEEE Real-Time Systems Symposium, 244–56. IEEE, 2020. https://doi.org/10.1109/RTSS49844.2020.00031."},"publication":"2020 IEEE Real-Time Systems Symposium","date_published":"2020-12-01T00:00:00Z","has_accepted_license":"1","article_processing_charge":"No","day":"01","ddc":["000"],"title":"Hybridization for stability verification of nonlinear switched systems","status":"public","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","_id":"9202","file":[{"relation":"main_file","file_id":"9203","date_created":"2021-02-26T16:38:14Z","date_updated":"2021-02-26T16:38:14Z","checksum":"8f97f229316c3b3a6f0cf99297aa0941","file_name":"main.pdf","access_level":"open_access","content_type":"application/pdf","file_size":1125794,"creator":"mgarcias"}],"oa_version":"Submitted Version","type":"conference","abstract":[{"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.","lang":"eng"}]},{"intvolume":" 36","ddc":["000"],"status":"public","title":"Abstraction based verification of stability of polyhedral switched systems","_id":"7426","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","file":[{"checksum":"560abfddb53f9fe921b6744f59f2cfaa","date_created":"2020-10-21T13:16:45Z","date_updated":"2022-05-16T22:30:04Z","relation":"main_file","embargo":"2022-05-15","file_id":"8688","file_size":818774,"content_type":"application/pdf","creator":"dernst","access_level":"open_access","file_name":"2020_NAHS_GarciaSoto.pdf"}],"oa_version":"Submitted Version","type":"journal_article","issue":"5","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"}],"article_type":"original","citation":{"apa":"Garcia Soto, M., & Prabhakar, P. (2020). Abstraction based verification of stability of polyhedral switched systems. Nonlinear Analysis: Hybrid Systems. Elsevier. https://doi.org/10.1016/j.nahs.2020.100856","ieee":"M. Garcia Soto and P. Prabhakar, “Abstraction based verification of stability of polyhedral switched systems,” Nonlinear Analysis: Hybrid Systems, vol. 36, no. 5. Elsevier, 2020.","ista":"Garcia Soto M, Prabhakar P. 2020. Abstraction based verification of stability of polyhedral switched systems. Nonlinear Analysis: Hybrid Systems. 36(5), 100856.","ama":"Garcia Soto M, Prabhakar P. Abstraction based verification of stability of polyhedral switched systems. Nonlinear Analysis: Hybrid Systems. 2020;36(5). doi:10.1016/j.nahs.2020.100856","chicago":"Garcia Soto, Miriam, and Pavithra Prabhakar. “Abstraction Based Verification of Stability of Polyhedral Switched Systems.” Nonlinear Analysis: Hybrid Systems. Elsevier, 2020. https://doi.org/10.1016/j.nahs.2020.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.” Nonlinear Analysis: Hybrid Systems, vol. 36, no. 5, 100856, Elsevier, 2020, doi:10.1016/j.nahs.2020.100856."},"publication":"Nonlinear Analysis: Hybrid Systems","date_published":"2020-05-01T00:00:00Z","scopus_import":"1","has_accepted_license":"1","article_processing_charge":"No","day":"01","publisher":"Elsevier","department":[{"_id":"ToHe"}],"publication_status":"published","year":"2020","volume":36,"date_created":"2020-02-02T23:00:59Z","date_updated":"2023-08-17T14:32:54Z","author":[{"full_name":"Garcia Soto, Miriam","orcid":"0000−0003−2936−5719","id":"4B3207F6-F248-11E8-B48F-1D18A9856A87","last_name":"Garcia Soto","first_name":"Miriam"},{"last_name":"Prabhakar","first_name":"Pavithra","full_name":"Prabhakar, Pavithra"}],"article_number":"100856","file_date_updated":"2022-05-16T22:30:04Z","project":[{"call_identifier":"FWF","name":"Game Theory","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"},{"name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"quality_controlled":"1","isi":1,"tmp":{"name":"Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International (CC BY-NC-ND 4.0)","legal_code_url":"https://creativecommons.org/licenses/by-nc-nd/4.0/legalcode","short":"CC BY-NC-ND (4.0)","image":"/images/cc_by_nc_nd.png"},"external_id":{"isi":["000528828600003"]},"oa":1,"language":[{"iso":"eng"}],"doi":"10.1016/j.nahs.2020.100856","publication_identifier":{"issn":["1751-570X"]},"month":"05"},{"oa":1,"quality_controlled":"1","project":[{"call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"conference":{"end_date":"2019-01-11","location":"Delhi, India","start_date":"2019-01-09","name":"ICC 2019 - Indian Control Conference"},"doi":"10.1109/INDIANCC.2019.8715598","language":[{"iso":"eng"}],"month":"05","publication_identifier":{"isbn":["978-153866246-5"]},"year":"2019","publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"IEEE","author":[{"last_name":"Kundu","first_name":"Atreyee","full_name":"Kundu, Atreyee"},{"full_name":"Garcia Soto, Miriam","last_name":"Garcia Soto","first_name":"Miriam","orcid":"0000−0003−2936−5719","id":"4B3207F6-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Prabhakar, Pavithra","last_name":"Prabhakar","first_name":"Pavithra"}],"date_created":"2019-06-17T06:57:33Z","date_updated":"2021-01-12T08:08:01Z","article_number":"8715598","file_date_updated":"2020-10-21T13:13:49Z","publication":"5th Indian Control Conference Proceedings","citation":{"ama":"Kundu A, Garcia Soto M, Prabhakar P. Formal synthesis of stabilizing controllers for periodically controlled linear switched systems. In: 5th Indian Control Conference Proceedings. IEEE; 2019. doi:10.1109/INDIANCC.2019.8715598","ieee":"A. Kundu, M. Garcia Soto, and P. Prabhakar, “Formal synthesis of stabilizing controllers for periodically controlled linear switched systems,” in 5th Indian Control Conference Proceedings, Delhi, India, 2019.","apa":"Kundu, A., Garcia Soto, M., & Prabhakar, P. (2019). Formal synthesis of stabilizing controllers for periodically controlled linear switched systems. In 5th Indian Control Conference Proceedings. Delhi, India: IEEE. https://doi.org/10.1109/INDIANCC.2019.8715598","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.","short":"A. Kundu, M. Garcia Soto, P. Prabhakar, in:, 5th Indian Control Conference Proceedings, IEEE, 2019.","mla":"Kundu, Atreyee, et al. “Formal Synthesis of Stabilizing Controllers for Periodically Controlled Linear Switched Systems.” 5th Indian Control Conference Proceedings, 8715598, IEEE, 2019, doi:10.1109/INDIANCC.2019.8715598.","chicago":"Kundu, Atreyee, Miriam Garcia Soto, and Pavithra Prabhakar. “Formal Synthesis of Stabilizing Controllers for Periodically Controlled Linear Switched Systems.” In 5th Indian Control Conference Proceedings. IEEE, 2019. https://doi.org/10.1109/INDIANCC.2019.8715598."},"date_published":"2019-05-16T00:00:00Z","scopus_import":"1","day":"16","has_accepted_license":"1","article_processing_charge":"No","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","_id":"6565","title":"Formal synthesis of stabilizing controllers for periodically controlled linear switched systems","ddc":["000"],"status":"public","file":[{"relation":"main_file","file_id":"8687","checksum":"d622a91af1e427f6b1e0ba8e18a2b767","success":1,"date_created":"2020-10-21T13:13:49Z","date_updated":"2020-10-21T13:13:49Z","access_level":"open_access","file_name":"2019_ICC_Kundu.pdf","content_type":"application/pdf","file_size":396031,"creator":"dernst"}],"oa_version":"Submitted Version","type":"conference","abstract":[{"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.","lang":"eng"}]},{"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.","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.","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","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"},"page":"297-314","date_published":"2019-07-12T00:00:00Z","scopus_import":"1","keyword":["Synthesis","Linear hybrid automaton","Membership"],"day":"12","article_processing_charge":"No","has_accepted_license":"1","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","_id":"6493","ddc":["000"],"title":"Membership-based synthesis of linear hybrid automata","status":"public","intvolume":" 11561","file":[{"checksum":"1f1d61b83a151031745ef70a501da3d6","date_created":"2019-08-14T11:05:30Z","date_updated":"2020-07-14T12:47:32Z","file_id":"6817","relation":"main_file","creator":"dernst","content_type":"application/pdf","file_size":674795,"access_level":"open_access","file_name":"2019_CAV_GarciaSoto.pdf"}],"oa_version":"Published Version","type":"conference","alternative_title":["LNCS"],"abstract":[{"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.","lang":"eng"}],"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,"isi":1,"quality_controlled":"1","project":[{"_id":"260C2330-B435-11E9-9278-68D0E5697425","grant_number":"754411","call_identifier":"H2020","name":"ISTplus - Postdoctoral Fellowships"},{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"},{"call_identifier":"FWF","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211"}],"conference":{"name":"CAV: Computer-Aided Verification","end_date":"2019-07-18","start_date":"2019-07-15","location":"New York City, NY, USA"},"doi":"10.1007/978-3-030-25540-4_16","language":[{"iso":"eng"}],"month":"07","publication_identifier":{"issn":["0302-9743"],"isbn":["9783030255398"]},"year":"2019","publication_status":"published","department":[{"_id":"ToHe"}],"publisher":"Springer","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"},{"first_name":"Christian","last_name":"Schilling","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian"},{"full_name":"Zeleznik, Luka","last_name":"Zeleznik","first_name":"Luka","id":"3ADCA2E4-F248-11E8-B48F-1D18A9856A87"}],"date_created":"2019-05-27T07:09:53Z","date_updated":"2023-08-25T10:40:41Z","volume":11561,"file_date_updated":"2020-07-14T12:47:32Z","ec_funded":1}]