[{"publication":"International Journal on Software Tools for Technology Transfer","day":"01","year":"2023","isi":1,"has_accepted_license":"1","date_created":"2023-07-16T22:01:11Z","date_published":"2023-08-01T00:00:00Z","doi":"10.1007/s10009-023-00711-4","page":"575-592","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, by DIREC - Digital Research Centre Denmark, and by the Villum Investigator Grant S4OS.","oa":1,"publisher":"Springer Nature","quality_controlled":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"short":"K. Kueffner, A. Lukina, C. Schilling, T.A. Henzinger, International Journal on Software Tools for Technology Transfer 25 (2023) 575–592.","ieee":"K. Kueffner, A. Lukina, C. Schilling, and T. A. Henzinger, “Into the unknown: Active monitoring of neural networks (extended version),” International Journal on Software Tools for Technology Transfer, vol. 25. Springer Nature, pp. 575–592, 2023.","apa":"Kueffner, K., Lukina, A., Schilling, C., & Henzinger, T. A. (2023). Into the unknown: Active monitoring of neural networks (extended version). International Journal on Software Tools for Technology Transfer. Springer Nature. https://doi.org/10.1007/s10009-023-00711-4","ama":"Kueffner K, Lukina A, Schilling C, Henzinger TA. Into the unknown: Active monitoring of neural networks (extended version). International Journal on Software Tools for Technology Transfer. 2023;25:575-592. doi:10.1007/s10009-023-00711-4","mla":"Kueffner, Konstantin, et al. “Into the Unknown: Active Monitoring of Neural Networks (Extended Version).” International Journal on Software Tools for Technology Transfer, vol. 25, Springer Nature, 2023, pp. 575–92, doi:10.1007/s10009-023-00711-4.","ista":"Kueffner K, Lukina A, Schilling C, Henzinger TA. 2023. Into the unknown: Active monitoring of neural networks (extended version). International Journal on Software Tools for Technology Transfer. 25, 575–592.","chicago":"Kueffner, Konstantin, Anna Lukina, Christian Schilling, and Thomas A Henzinger. “Into the Unknown: Active Monitoring of Neural Networks (Extended Version).” International Journal on Software Tools for Technology Transfer. Springer Nature, 2023. https://doi.org/10.1007/s10009-023-00711-4."},"title":"Into the unknown: Active monitoring of neural networks (extended version)","external_id":{"arxiv":["2009.06429"],"isi":["001020160000001"]},"article_processing_charge":"Yes (in subscription journal)","author":[{"first_name":"Konstantin","id":"8121a2d0-dc85-11ea-9058-af578f3b4515","last_name":"Kueffner","orcid":"0000-0001-8974-2542","full_name":"Kueffner, Konstantin"},{"full_name":"Lukina, Anna","last_name":"Lukina","first_name":"Anna","id":"CBA4D1A8-0FE8-11E9-BDE6-07BFE5697425"},{"first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian","last_name":"Schilling"},{"orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"}],"project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"}],"language":[{"iso":"eng"}],"file":[{"date_created":"2024-01-30T12:06:07Z","file_name":"2023_JourSoftwareTools_Kueffner.pdf","date_updated":"2024-01-30T12:06:07Z","file_size":13387667,"creator":"dernst","checksum":"3c4b347f39412a76872f9a6f30101f94","file_id":"14903","success":1,"content_type":"application/pdf","access_level":"open_access","relation":"main_file"}],"publication_status":"published","publication_identifier":{"eissn":["1433-2787"],"issn":["1433-2779"]},"ec_funded":1,"related_material":{"record":[{"relation":"shorter_version","status":"public","id":"10206"}]},"volume":25,"oa_version":"Published Version","abstract":[{"text":"Neural-network classifiers achieve high accuracy when predicting the class of an input that they were trained to identify. Maintaining this accuracy in dynamic environments, where inputs frequently fall outside the fixed set of initially known classes, remains a challenge. We consider the problem of monitoring the classification decisions of neural networks in the presence of novel classes. For this purpose, we generalize our recently proposed abstraction-based monitor from binary output to real-valued quantitative output. This quantitative output enables new applications, two of which we investigate in the paper. As our first application, we introduce an algorithmic framework for active monitoring of a neural network, which allows us to learn new classes dynamically and yet maintain high monitoring performance. As our second application, we present an offline procedure to retrain the neural network to improve the monitor’s detection performance without deteriorating the network’s classification accuracy. Our experimental evaluation demonstrates both the benefits of our active monitoring framework in dynamic scenarios and the effectiveness of the retraining procedure.","lang":"eng"}],"intvolume":" 25","month":"08","scopus_import":"1","ddc":["000"],"date_updated":"2024-01-30T12:06:57Z","department":[{"_id":"ToHe"}],"file_date_updated":"2024-01-30T12:06:07Z","_id":"13234","status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"article_type":"original","type":"journal_article"},{"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."}],"oa_version":"Preprint","scopus_import":"1","alternative_title":["LNCS"],"main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2208.06383"}],"month":"10","intvolume":" 13505","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031199912"],"eisbn":["9783031199929"]},"publication_status":"published","language":[{"iso":"eng"}],"volume":13505,"ec_funded":1,"_id":"12171","type":"conference","conference":{"name":"ATVA: Automated Technology for Verification and Analysis","start_date":"2022-10-25","end_date":"2022-10-28","location":"Virtual"},"status":"public","date_updated":"2023-02-13T09:27:55Z","department":[{"_id":"ToHe"}],"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.","publisher":"Springer Nature","quality_controlled":"1","oa":1,"year":"2022","day":"21","publication":"20th International Symposium on Automated Technology for Verification and Analysis","page":"337-353","date_published":"2022-10-21T00:00:00Z","doi":"10.1007/978-3-031-19992-9_22","date_created":"2023-01-12T12:11:16Z","project":[{"call_identifier":"H2020","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"citation":{"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.","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.","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","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","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."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"first_name":"Miriam","id":"4B3207F6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-2936-5719","full_name":"Garcia Soto, Miriam","last_name":"Garcia Soto"},{"first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger"},{"orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian","last_name":"Schilling","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","first_name":"Christian"}],"external_id":{"arxiv":["2208.06383"]},"article_processing_charge":"No","title":"Synthesis of parametric hybrid automata from time series"},{"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.","publisher":"Association for Computing Machinery","quality_controlled":"1","oa":1,"day":"01","publication":"HSCC '21: Proceedings of the 24th International Conference on Hybrid Systems: Computation and Control","has_accepted_license":"1","isi":1,"year":"2021","doi":"10.1145/3447928.3456704","date_published":"2021-05-01T00:00:00Z","date_created":"2021-02-26T16:30:39Z","page":"2102.12734","project":[{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"},{"call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425","grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships"}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"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.","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.","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.","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.","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."},"title":"Synthesis of hybrid automata with affine dynamics from time-series data","author":[{"first_name":"Miriam","id":"4B3207F6-F248-11E8-B48F-1D18A9856A87","last_name":"Garcia Soto","orcid":"0000-0003-2936-5719","full_name":"Garcia Soto, Miriam"},{"orcid":"0000-0002-2985-7724","full_name":"Henzinger, Thomas A","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","full_name":"Schilling, Christian","orcid":"0000-0003-3658-1065","last_name":"Schilling"}],"external_id":{"isi":["000932821700028"],"arxiv":["2102.12734"]},"article_processing_charge":"No","oa_version":"Published Version","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."}],"month":"05","scopus_import":"1","file":[{"date_created":"2021-05-25T13:53:22Z","file_name":"2021_HSCC_Soto.pdf","date_updated":"2021-05-25T13:53:22Z","file_size":1474786,"creator":"kschuh","file_id":"9424","checksum":"4c1202c1abf71384c3ee6fea88c2f80e","success":1,"content_type":"application/pdf","access_level":"open_access","relation":"main_file"}],"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["9781450383394"]},"publication_status":"published","ec_funded":1,"_id":"9200","status":"public","keyword":["hybrid automaton","membership","system identification"],"type":"conference","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"start_date":"2021-05-19","end_date":"2021-05-21","location":"Nashville, TN, United States","name":"HSCC: International Conference on Hybrid Systems Computation and Control"},"ddc":["000"],"date_updated":"2023-08-07T13:49:33Z","file_date_updated":"2021-05-25T13:53:22Z","department":[{"_id":"ToHe"}]},{"page":"42-61","date_created":"2021-10-31T23:01:31Z","date_published":"2021-10-06T00:00:00Z","doi":"10.1007/978-3-030-88494-9_3","year":"2021","isi":1,"publication":"21st International Conference on Runtime Verification","day":"06","oa":1,"publisher":"Springer Nature","quality_controlled":"1","acknowledgement":"We thank Christoph Lampert and Alex Greengold for fruitful discussions. This research was supported in part by the Simons Institute for the Theory of Computing, 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.","external_id":{"arxiv":["2009.06429"],"isi":["000719383800003"]},"article_processing_charge":"No","author":[{"first_name":"Anna","id":"CBA4D1A8-0FE8-11E9-BDE6-07BFE5697425","last_name":"Lukina","full_name":"Lukina, Anna"},{"last_name":"Schilling","orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","first_name":"Christian"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger"}],"title":"Into the unknown: active monitoring of neural networks","citation":{"chicago":"Lukina, Anna, Christian Schilling, and Thomas A Henzinger. “Into the Unknown: Active Monitoring of Neural Networks.” In 21st International Conference on Runtime Verification, 12974:42–61. Cham: Springer Nature, 2021. https://doi.org/10.1007/978-3-030-88494-9_3.","ista":"Lukina A, Schilling C, Henzinger TA. 2021. Into the unknown: active monitoring of neural networks. 21st International Conference on Runtime Verification. RV: Runtime Verification, LNCS, vol. 12974, 42–61.","mla":"Lukina, Anna, et al. “Into the Unknown: Active Monitoring of Neural Networks.” 21st International Conference on Runtime Verification, vol. 12974, Springer Nature, 2021, pp. 42–61, doi:10.1007/978-3-030-88494-9_3.","ama":"Lukina A, Schilling C, Henzinger TA. Into the unknown: active monitoring of neural networks. In: 21st International Conference on Runtime Verification. Vol 12974. Cham: Springer Nature; 2021:42-61. doi:10.1007/978-3-030-88494-9_3","apa":"Lukina, A., Schilling, C., & Henzinger, T. A. (2021). Into the unknown: active monitoring of neural networks. In 21st International Conference on Runtime Verification (Vol. 12974, pp. 42–61). Cham: Springer Nature. https://doi.org/10.1007/978-3-030-88494-9_3","short":"A. Lukina, C. Schilling, T.A. Henzinger, in:, 21st International Conference on Runtime Verification, Springer Nature, Cham, 2021, pp. 42–61.","ieee":"A. Lukina, C. Schilling, and T. A. Henzinger, “Into the unknown: active monitoring of neural networks,” in 21st International Conference on Runtime Verification, Virtual, 2021, vol. 12974, pp. 42–61."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","project":[{"call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425","name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"}],"ec_funded":1,"volume":"12974 ","related_material":{"record":[{"relation":"extended_version","id":"13234","status":"public"}]},"publication_status":"published","publication_identifier":{"issn":["0302-9743"],"isbn":["9-783-0308-8493-2"],"eissn":["1611-3349"],"eisbn":["978-3-030-88494-9"]},"language":[{"iso":"eng"}],"main_file_link":[{"url":"https://arxiv.org/abs/2009.06429","open_access":"1"}],"scopus_import":"1","alternative_title":["LNCS"],"place":"Cham","month":"10","abstract":[{"text":"Neural-network classifiers achieve high accuracy when predicting the class of an input that they were trained to identify. Maintaining this accuracy in dynamic environments, where inputs frequently fall outside the fixed set of initially known classes, remains a challenge. The typical approach is to detect inputs from novel classes and retrain the classifier on an augmented dataset. However, not only the classifier but also the detection mechanism needs to adapt in order to distinguish between newly learned and yet unknown input classes. To address this challenge, we introduce an algorithmic framework for active monitoring of a neural network. A monitor wrapped in our framework operates in parallel with the neural network and interacts with a human user via a series of interpretable labeling queries for incremental adaptation. In addition, we propose an adaptive quantitative monitor to improve precision. An experimental evaluation on a diverse set of benchmarks with varying numbers of classes confirms the benefits of our active monitoring framework in dynamic scenarios.","lang":"eng"}],"oa_version":"Preprint","department":[{"_id":"ToHe"}],"date_updated":"2024-01-30T12:06:56Z","conference":{"name":"RV: Runtime Verification","end_date":"2021-10-14","location":"Virtual","start_date":"2021-10-11"},"type":"conference","keyword":["monitoring","neural networks","novelty detection"],"status":"public","_id":"10206"},{"publication":"EPiC Series in Computing","day":"25","year":"2020","date_created":"2020-09-26T14:49:43Z","doi":"10.29007/7dt2","date_published":"2020-09-25T00:00:00Z","page":"16-48","acknowledgement":"The authors gratefully acknowledge financial support by the European Commission project\r\njustITSELF under grant number 817629, by the Austrian Science Fund (FWF) under grant\r\nZ211-N23 (Wittgenstein Award), by the European Union’s Horizon 2020 research and innovation programme under the Marie Sk lodowska-Curie grant agreement No. 754411, and by the\r\nScience and Engineering Research Board (SERB) project with file number IMP/2018/000523.\r\nThis material is based upon work supported by the Air Force Office of Scientific Research under\r\naward number FA9550-19-1-0288. Any opinions, finding, and conclusions or recommendations\r\nexpressed in this material are those of the author(s) and do not necessarily reflect the views of\r\nthe United States Air Force.","oa":1,"quality_controlled":"1","publisher":"EasyChair","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ieee":"M. Althoff et al., “ARCH-COMP20 Category Report: Continuous and hybrid systems with linear dynamics,” in EPiC Series in Computing, 2020, vol. 74, pp. 16–48.","short":"M. Althoff, S. Bak, Z. Bao, M. Forets, G. Frehse, D. Freire, N. Kochdumper, Y. Li, S. Mitra, R. Ray, C. Schilling, S. Schupp, M. Wetzlinger, in:, EPiC Series in Computing, EasyChair, 2020, pp. 16–48.","apa":"Althoff, M., Bak, S., Bao, Z., Forets, M., Frehse, G., Freire, D., … Wetzlinger, M. (2020). ARCH-COMP20 Category Report: Continuous and hybrid systems with linear dynamics. In EPiC Series in Computing (Vol. 74, pp. 16–48). EasyChair. https://doi.org/10.29007/7dt2","ama":"Althoff M, Bak S, Bao Z, et al. ARCH-COMP20 Category Report: Continuous and hybrid systems with linear dynamics. In: EPiC Series in Computing. Vol 74. EasyChair; 2020:16-48. doi:10.29007/7dt2","mla":"Althoff, Matthias, et al. “ARCH-COMP20 Category Report: Continuous and Hybrid Systems with Linear Dynamics.” EPiC Series in Computing, vol. 74, EasyChair, 2020, pp. 16–48, doi:10.29007/7dt2.","ista":"Althoff M, Bak S, Bao Z, Forets M, Frehse G, Freire D, Kochdumper N, Li Y, Mitra S, Ray R, Schilling C, Schupp S, Wetzlinger M. 2020. ARCH-COMP20 Category Report: Continuous and hybrid systems with linear dynamics. EPiC Series in Computing. ARCH: International Workshop on Applied Verification on Continuous and Hybrid Systems vol. 74, 16–48.","chicago":"Althoff, Matthias, Stanley Bak, Zongnan Bao, Marcelo Forets, Goran Frehse, Daniel Freire, Niklas Kochdumper, et al. “ARCH-COMP20 Category Report: Continuous and Hybrid Systems with Linear Dynamics.” In EPiC Series in Computing, 74:16–48. EasyChair, 2020. https://doi.org/10.29007/7dt2."},"title":"ARCH-COMP20 Category Report: Continuous and hybrid systems with linear dynamics","article_processing_charge":"No","author":[{"first_name":"Matthias","full_name":"Althoff, Matthias","last_name":"Althoff"},{"first_name":"Stanley","full_name":"Bak, Stanley","last_name":"Bak"},{"first_name":"Zongnan","last_name":"Bao","full_name":"Bao, Zongnan"},{"full_name":"Forets, Marcelo","last_name":"Forets","first_name":"Marcelo"},{"first_name":"Goran","last_name":"Frehse","full_name":"Frehse, Goran"},{"first_name":"Daniel","last_name":"Freire","full_name":"Freire, Daniel"},{"first_name":"Niklas","last_name":"Kochdumper","full_name":"Kochdumper, Niklas"},{"full_name":"Li, Yangge","last_name":"Li","first_name":"Yangge"},{"first_name":"Sayan","full_name":"Mitra, Sayan","last_name":"Mitra"},{"first_name":"Rajarshi","full_name":"Ray, Rajarshi","last_name":"Ray"},{"first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","last_name":"Schilling","orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian"},{"first_name":"Stefan","full_name":"Schupp, Stefan","last_name":"Schupp"},{"last_name":"Wetzlinger","full_name":"Wetzlinger, Mark","first_name":"Mark"}],"project":[{"call_identifier":"FWF","_id":"25C5A090-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z00312"},{"call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425","name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411"}],"language":[{"iso":"eng"}],"publication_status":"published","ec_funded":1,"volume":74,"oa_version":"Published Version","abstract":[{"lang":"eng","text":"We present the results of the ARCH 2020 friendly competition for formal verification of continuous and hybrid systems with linear continuous dynamics. In its fourth edition, eight tools have been applied to solve eight different benchmark problems in the category for linear continuous dynamics (in alphabetical order): CORA, C2E2, HyDRA, Hylaa, Hylaa-Continuous, JuliaReach, SpaceEx, and XSpeed. This report is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results provide one of the most complete assessments of tools for the safety verification of continuous and hybrid systems with linear continuous dynamics up to this date."}],"intvolume":" 74","month":"09","main_file_link":[{"url":"https://easychair.org/publications/download/DRpS","open_access":"1"}],"date_updated":"2021-01-12T08:20:06Z","department":[{"_id":"ToHe"}],"_id":"8572","status":"public","conference":{"name":"ARCH: International Workshop on Applied Verification on Continuous and Hybrid Systems","end_date":"2020-07-12","start_date":"2020-07-12"},"type":"conference"},{"project":[{"_id":"260C2330-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"}],"article_processing_charge":"No","author":[{"first_name":"Luca","last_name":"Geretti","full_name":"Geretti, Luca"},{"first_name":"Julien","last_name":"Alexandre Dit Sandretto","full_name":"Alexandre Dit Sandretto, Julien"},{"full_name":"Althoff, Matthias","last_name":"Althoff","first_name":"Matthias"},{"last_name":"Benet","full_name":"Benet, Luis","first_name":"Luis"},{"first_name":"Alexandre","full_name":"Chapoutot, Alexandre","last_name":"Chapoutot"},{"first_name":"Xin","full_name":"Chen, Xin","last_name":"Chen"},{"first_name":"Pieter","last_name":"Collins","full_name":"Collins, Pieter"},{"first_name":"Marcelo","full_name":"Forets, Marcelo","last_name":"Forets"},{"full_name":"Freire, Daniel","last_name":"Freire","first_name":"Daniel"},{"first_name":"Fabian","full_name":"Immler, Fabian","last_name":"Immler"},{"last_name":"Kochdumper","full_name":"Kochdumper, Niklas","first_name":"Niklas"},{"first_name":"David","last_name":"Sanders","full_name":"Sanders, David"},{"first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","full_name":"Schilling, Christian","orcid":"0000-0003-3658-1065","last_name":"Schilling"}],"title":"ARCH-COMP20 Category Report: Continuous and hybrid systems with nonlinear dynamics","citation":{"chicago":"Geretti, Luca, Julien Alexandre Dit Sandretto, Matthias Althoff, Luis Benet, Alexandre Chapoutot, Xin Chen, Pieter Collins, et al. “ARCH-COMP20 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics.” In EPiC Series in Computing, 74:49–75. EasyChair, 2020. https://doi.org/10.29007/zkf6.","ista":"Geretti L, Alexandre Dit Sandretto J, Althoff M, Benet L, Chapoutot A, Chen X, Collins P, Forets M, Freire D, Immler F, Kochdumper N, Sanders D, Schilling C. 2020. ARCH-COMP20 Category Report: Continuous and hybrid systems with nonlinear dynamics. EPiC Series in Computing. ARCH: International Workshop on Applied Verification on Continuous and Hybrid Systems vol. 74, 49–75.","mla":"Geretti, Luca, et al. “ARCH-COMP20 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics.” EPiC Series in Computing, vol. 74, EasyChair, 2020, pp. 49–75, doi:10.29007/zkf6.","short":"L. Geretti, J. Alexandre Dit Sandretto, M. Althoff, L. Benet, A. Chapoutot, X. Chen, P. Collins, M. Forets, D. Freire, F. Immler, N. Kochdumper, D. Sanders, C. Schilling, in:, EPiC Series in Computing, EasyChair, 2020, pp. 49–75.","ieee":"L. Geretti et al., “ARCH-COMP20 Category Report: Continuous and hybrid systems with nonlinear dynamics,” in EPiC Series in Computing, 2020, vol. 74, pp. 49–75.","ama":"Geretti L, Alexandre Dit Sandretto J, Althoff M, et al. ARCH-COMP20 Category Report: Continuous and hybrid systems with nonlinear dynamics. In: EPiC Series in Computing. Vol 74. EasyChair; 2020:49-75. doi:10.29007/zkf6","apa":"Geretti, L., Alexandre Dit Sandretto, J., Althoff, M., Benet, L., Chapoutot, A., Chen, X., … Schilling, C. (2020). ARCH-COMP20 Category Report: Continuous and hybrid systems with nonlinear dynamics. In EPiC Series in Computing (Vol. 74, pp. 49–75). EasyChair. https://doi.org/10.29007/zkf6"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","oa":1,"quality_controlled":"1","publisher":"EasyChair","acknowledgement":"Christian Schilling acknowledges support 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 lodowska-Curie grant agreement No. 754411.","page":"49-75","date_created":"2020-09-26T14:41:29Z","date_published":"2020-09-25T00:00:00Z","doi":"10.29007/zkf6","year":"2020","publication":"EPiC Series in Computing","day":"25","conference":{"name":"ARCH: International Workshop on Applied Verification on Continuous and Hybrid Systems","start_date":"2020-07-12","end_date":"2020-07-12"},"type":"conference","status":"public","_id":"8571","department":[{"_id":"ToHe"}],"date_updated":"2021-01-12T08:20:06Z","main_file_link":[{"url":"https://easychair.org/publications/download/nrdD","open_access":"1"}],"intvolume":" 74","month":"09","abstract":[{"lang":"eng","text":"We present the results of a friendly competition for formal verification of continuous and hybrid systems with nonlinear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2020. This year, 6 tools Ariadne, CORA, DynIbex, Flow*, Isabelle/HOL, and JuliaReach (in alphabetic order) participated. These tools are applied to solve reachability analysis problems on six benchmark problems, two of them featuring hybrid dynamics. We do not rank the tools based on the results, but show the current status and discover the potential advantages of different tools."}],"oa_version":"Published Version","ec_funded":1,"volume":74,"publication_status":"published","language":[{"iso":"eng"}]},{"doi":"10.3233/FAIA200375","date_published":"2020-02-24T00:00:00Z","date_created":"2020-02-21T16:44:03Z","page":"2433-2440","day":"24","publication":"24th European Conference on Artificial Intelligence","isi":1,"has_accepted_license":"1","year":"2020","quality_controlled":"1","publisher":"IOS Press","oa":1,"acknowledgement":"We thank Christoph Lampert and Nikolaus Mayer for fruitful discussions. This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award) and the European Union’s Horizon 2020 research and innovation programme under the Marie SkłodowskaCurie grant agreement No. 754411.","title":"Outside the box: Abstraction-based monitoring of neural networks","author":[{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A","full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger"},{"last_name":"Lukina","full_name":"Lukina, Anna","id":"CBA4D1A8-0FE8-11E9-BDE6-07BFE5697425","first_name":"Anna"},{"full_name":"Schilling, Christian","orcid":"0000-0003-3658-1065","last_name":"Schilling","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","first_name":"Christian"}],"external_id":{"isi":["000650971303002"],"arxiv":["1911.09032"]},"article_processing_charge":"No","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"mla":"Henzinger, Thomas A., et al. “Outside the Box: Abstraction-Based Monitoring of Neural Networks.” 24th European Conference on Artificial Intelligence, vol. 325, IOS Press, 2020, pp. 2433–40, doi:10.3233/FAIA200375.","apa":"Henzinger, T. A., Lukina, A., & Schilling, C. (2020). Outside the box: Abstraction-based monitoring of neural networks. In 24th European Conference on Artificial Intelligence (Vol. 325, pp. 2433–2440). Santiago de Compostela, Spain: IOS Press. https://doi.org/10.3233/FAIA200375","ama":"Henzinger TA, Lukina A, Schilling C. Outside the box: Abstraction-based monitoring of neural networks. In: 24th European Conference on Artificial Intelligence. Vol 325. IOS Press; 2020:2433-2440. doi:10.3233/FAIA200375","ieee":"T. A. Henzinger, A. Lukina, and C. Schilling, “Outside the box: Abstraction-based monitoring of neural networks,” in 24th European Conference on Artificial Intelligence, Santiago de Compostela, Spain, 2020, vol. 325, pp. 2433–2440.","short":"T.A. Henzinger, A. Lukina, C. Schilling, in:, 24th European Conference on Artificial Intelligence, IOS Press, 2020, pp. 2433–2440.","chicago":"Henzinger, Thomas A, Anna Lukina, and Christian Schilling. “Outside the Box: Abstraction-Based Monitoring of Neural Networks.” In 24th European Conference on Artificial Intelligence, 325:2433–40. IOS Press, 2020. https://doi.org/10.3233/FAIA200375.","ista":"Henzinger TA, Lukina A, Schilling C. 2020. Outside the box: Abstraction-based monitoring of neural networks. 24th European Conference on Artificial Intelligence. ECAI: European Conference on Artificial Intelligence, Frontiers in Artificial Intelligence and Applications, vol. 325, 2433–2440."},"project":[{"name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411","_id":"260C2330-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","grant_number":"Z211","name":"The Wittgenstein Prize"}],"volume":325,"ec_funded":1,"license":"https://creativecommons.org/licenses/by-nc/4.0/","file":[{"content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"80642fa0b6cd7da95dcd87d63789ad5e","file_id":"8540","success":1,"date_updated":"2020-09-21T07:12:32Z","file_size":1692214,"creator":"dernst","date_created":"2020-09-21T07:12:32Z","file_name":"2020_ECAI_Henzinger.pdf"}],"language":[{"iso":"eng"}],"publication_status":"published","month":"02","intvolume":" 325","alternative_title":["Frontiers in Artificial Intelligence and Applications"],"oa_version":"Published Version","abstract":[{"text":"Neural networks have demonstrated unmatched performance in a range of classification tasks. Despite numerous efforts of the research community, novelty detection remains one of the significant limitations of neural networks. The ability to identify previously unseen inputs as novel is crucial for our understanding of the decisions made by neural networks. At runtime, inputs not falling into any of the categories learned during training cannot be classified correctly by the neural network. Existing approaches treat the neural network as a black box and try to detect novel inputs based on the confidence of the output predictions. However, neural networks are not trained to reduce their confidence for novel inputs, which limits the effectiveness of these approaches. We propose a framework to monitor a neural network by observing the hidden layers. We employ a common abstraction from program analysis - boxes - to identify novel behaviors in the monitored layers, i.e., inputs that cause behaviors outside the box. For each neuron, the boxes range over the values seen in training. The framework is efficient and flexible to achieve a desired trade-off between raising false warnings and detecting novel inputs. We illustrate the performance and the robustness to variability in the unknown classes on popular image-classification benchmarks.","lang":"eng"}],"file_date_updated":"2020-09-21T07:12:32Z","department":[{"_id":"ToHe"}],"ddc":["000"],"date_updated":"2023-08-18T06:38:16Z","status":"public","type":"conference","conference":{"start_date":"2020-08-29","end_date":"2020-09-08","location":"Santiago de Compostela, Spain","name":"ECAI: European Conference on Artificial Intelligence"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by-nc/4.0/legalcode","image":"/images/cc_by_nc.png","name":"Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0)","short":"CC BY-NC (4.0)"},"_id":"7505"},{"department":[{"_id":"ToHe"}],"date_updated":"2023-08-22T12:48:18Z","status":"public","type":"conference","conference":{"start_date":"2020-12-02","location":"Virtual Conference","end_date":"2020-12-04","name":"MEMOCODE: Conference on Formal Methods and Models for System Design"},"_id":"8750","ec_funded":1,"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["9781728191485"]},"publication_status":"published","month":"12","scopus_import":"1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2006.12325"}],"oa_version":"Preprint","abstract":[{"lang":"eng","text":"Efficiently handling time-triggered and possibly nondeterministic switches\r\nfor hybrid systems reachability is a challenging task. In this paper we present\r\nan approach based on conservative set-based enclosure of the dynamics that can\r\nhandle systems with uncertain parameters and inputs, where the uncertainties\r\nare bound to given intervals. The method is evaluated on the plant model of an\r\nexperimental electro-mechanical braking system with periodic controller. In\r\nthis model, the fast-switching controller dynamics requires simulation time\r\nscales of the order of nanoseconds. Accurate set-based computations for\r\nrelatively large time horizons are known to be expensive. However, by\r\nappropriately decoupling the time variable with respect to the spatial\r\nvariables, and enclosing the uncertain parameters using interval matrix maps\r\nacting on zonotopes, we show that the computation time can be lowered to 5000\r\ntimes faster with respect to previous works. This is a step forward in formal\r\nverification of hybrid systems because reduced run-times allow engineers to\r\nintroduce more expressiveness in their models with a relatively inexpensive\r\ncomputational cost."}],"title":"Efficient reachability analysis of parametric linear hybrid systems with time-triggered transitions","author":[{"first_name":"Marcelo","last_name":"Forets","full_name":"Forets, Marcelo"},{"full_name":"Freire, Daniel","last_name":"Freire","first_name":"Daniel"},{"id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","first_name":"Christian","last_name":"Schilling","full_name":"Schilling, Christian","orcid":"0000-0003-3658-1065"}],"article_processing_charge":"No","external_id":{"isi":["000661920400013"],"arxiv":["2006.12325"]},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"ista":"Forets M, Freire D, Schilling C. 2020. Efficient reachability analysis of parametric linear hybrid systems with time-triggered transitions. 18th ACM-IEEE International Conference on Formal Methods and Models for System Design. MEMOCODE: Conference on Formal Methods and Models for System Design, 9314994.","chicago":"Forets, Marcelo, Daniel Freire, and Christian Schilling. “Efficient Reachability Analysis of Parametric Linear Hybrid Systems with Time-Triggered Transitions.” In 18th ACM-IEEE International Conference on Formal Methods and Models for System Design. IEEE, 2020. https://doi.org/10.1109/MEMOCODE51338.2020.9314994.","ama":"Forets M, Freire D, Schilling C. Efficient reachability analysis of parametric linear hybrid systems with time-triggered transitions. In: 18th ACM-IEEE International Conference on Formal Methods and Models for System Design. IEEE; 2020. doi:10.1109/MEMOCODE51338.2020.9314994","apa":"Forets, M., Freire, D., & Schilling, C. (2020). Efficient reachability analysis of parametric linear hybrid systems with time-triggered transitions. In 18th ACM-IEEE International Conference on Formal Methods and Models for System Design. Virtual Conference: IEEE. https://doi.org/10.1109/MEMOCODE51338.2020.9314994","short":"M. Forets, D. Freire, C. Schilling, in:, 18th ACM-IEEE International Conference on Formal Methods and Models for System Design, IEEE, 2020.","ieee":"M. Forets, D. Freire, and C. Schilling, “Efficient reachability analysis of parametric linear hybrid systems with time-triggered transitions,” in 18th ACM-IEEE International Conference on Formal Methods and Models for System Design, Virtual Conference, 2020.","mla":"Forets, Marcelo, et al. “Efficient Reachability Analysis of Parametric Linear Hybrid Systems with Time-Triggered Transitions.” 18th ACM-IEEE International Conference on Formal Methods and Models for System Design, 9314994, IEEE, 2020, doi:10.1109/MEMOCODE51338.2020.9314994."},"project":[{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"Z211","name":"The Wittgenstein Prize"},{"call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425","name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411"}],"article_number":"9314994","date_published":"2020-12-04T00:00:00Z","doi":"10.1109/MEMOCODE51338.2020.9314994","date_created":"2020-11-10T07:04:57Z","day":"04","publication":"18th ACM-IEEE International Conference on Formal Methods and Models for System Design","isi":1,"year":"2020","publisher":"IEEE","quality_controlled":"1","oa":1},{"quality_controlled":"1","oa":1,"date_published":"2020-01-01T00:00:00Z","date_created":"2020-08-24T12:56:20Z","has_accepted_license":"1","year":"2020","publication":"Proceedings of the International Conference on Embedded Software","project":[{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"name":"The Wittgenstein Prize","grant_number":"Z00312","call_identifier":"FWF","_id":"25C5A090-B435-11E9-9278-68D0E5697425"},{"name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411","_id":"260C2330-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"}],"author":[{"first_name":"Sergiy","full_name":"Bogomolov, Sergiy","last_name":"Bogomolov"},{"last_name":"Forets","full_name":"Forets, Marcelo","first_name":"Marcelo"},{"last_name":"Frehse","full_name":"Frehse, Goran","first_name":"Goran"},{"first_name":"Kostiantyn","last_name":"Potomkin","full_name":"Potomkin, Kostiantyn"},{"first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","last_name":"Schilling","orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian"}],"external_id":{"arxiv":["1905.02458"]},"article_processing_charge":"No","title":"Reachability analysis of linear hybrid systems via block decomposition","citation":{"chicago":"Bogomolov, Sergiy, Marcelo Forets, Goran Frehse, Kostiantyn Potomkin, and Christian Schilling. “Reachability Analysis of Linear Hybrid Systems via Block Decomposition.” In Proceedings of the International Conference on Embedded Software, 2020.","ista":"Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. 2020. Reachability analysis of linear hybrid systems via block decomposition. Proceedings of the International Conference on Embedded Software. EMSOFT: International Conference on Embedded Software.","mla":"Bogomolov, Sergiy, et al. “Reachability Analysis of Linear Hybrid Systems via Block Decomposition.” Proceedings of the International Conference on Embedded Software, 2020.","ieee":"S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, and C. Schilling, “Reachability analysis of linear hybrid systems via block decomposition,” in Proceedings of the International Conference on Embedded Software, Virtual , 2020.","short":"S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, C. Schilling, in:, Proceedings of the International Conference on Embedded Software, 2020.","ama":"Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. Reachability analysis of linear hybrid systems via block decomposition. In: Proceedings of the International Conference on Embedded Software. ; 2020.","apa":"Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., & Schilling, C. (2020). Reachability analysis of linear hybrid systems via block decomposition. In Proceedings of the International Conference on Embedded Software. Virtual ."},"user_id":"8b945eb4-e2f2-11eb-945a-df72226e66a9","abstract":[{"text":"Reachability analysis aims at identifying states reachable by a system within a given time horizon. This task is known to be computationally expensive for linear hybrid systems. Reachability analysis works by iteratively applying continuous and discrete post operators to compute states reachable according to continuous and discrete dynamics, respectively. In this paper, we enhance both of these operators and make sure that most of the involved computations are performed in low-dimensional state space. In particular, we improve the continuous-post operator by performing computations in high-dimensional state space only for time intervals relevant for the subsequent application of the discrete-post operator. Furthermore, the new discrete-post operator performs low-dimensional computations by leveraging the structure of the guard and assignment of a considered transition. We illustrate the potential of our approach on a number of challenging benchmarks.","lang":"eng"}],"oa_version":"Preprint","related_material":{"record":[{"relation":"later_version","status":"public","id":"8790"}]},"ec_funded":1,"publication_status":"published","file":[{"checksum":"d19e97d0f8a3a441dc078ec812297d75","file_id":"8288","success":1,"access_level":"open_access","relation":"main_file","content_type":"application/pdf","date_created":"2020-08-24T12:53:15Z","file_name":"2020EMSOFT.pdf","creator":"cschilli","date_updated":"2020-08-24T12:53:15Z","file_size":696384}],"language":[{"iso":"eng"}],"type":"conference","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"location":"Virtual ","end_date":"2020-09-25","start_date":"2020-09-20","name":"EMSOFT: International Conference on Embedded Software"},"status":"public","keyword":["reachability","hybrid systems","decomposition"],"_id":"8287","department":[{"_id":"ToHe"}],"file_date_updated":"2020-08-24T12:53:15Z","date_updated":"2023-08-22T13:27:32Z","ddc":["000"]},{"publication_status":"published","publication_identifier":{"issn":["02780070"],"eissn":["19374151"]},"language":[{"iso":"eng"}],"ec_funded":1,"issue":"11","volume":39,"related_material":{"record":[{"status":"public","id":"8287","relation":"earlier_version"}]},"abstract":[{"text":"Reachability analysis aims at identifying states reachable by a system within a given time horizon. This task is known to be computationally expensive for linear hybrid systems. Reachability analysis works by iteratively applying continuous and discrete post operators to compute states reachable according to continuous and discrete dynamics, respectively. In this article, we enhance both of these operators and make sure that most of the involved computations are performed in low-dimensional state space. In particular, we improve the continuous-post operator by performing computations in high-dimensional state space only for time intervals relevant for the subsequent application of the discrete-post operator. Furthermore, the new discrete-post operator performs low-dimensional computations by leveraging the structure of the guard and assignment of a considered transition. We illustrate the potential of our approach on a number of challenging benchmarks.","lang":"eng"}],"oa_version":"Preprint","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1905.02458"}],"scopus_import":"1","intvolume":" 39","month":"11","date_updated":"2023-08-22T13:27:33Z","department":[{"_id":"ToHe"}],"_id":"8790","type":"journal_article","article_type":"original","status":"public","year":"2020","isi":1,"publication":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems","day":"01","page":"4018-4029","date_created":"2020-11-22T23:01:25Z","date_published":"2020-11-01T00:00:00Z","doi":"10.1109/TCAD.2020.3012859","acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No. 754411, and the Air Force Office of Scientific Research under award number FA2386-17-1-4065. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the United States Air Force. ","oa":1,"quality_controlled":"1","publisher":"IEEE","citation":{"ista":"Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. 2020. Reachability analysis of linear hybrid systems via block decomposition. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. 39(11), 4018–4029.","chicago":"Bogomolov, Sergiy, Marcelo Forets, Goran Frehse, Kostiantyn Potomkin, and Christian Schilling. “Reachability Analysis of Linear Hybrid Systems via Block Decomposition.” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. IEEE, 2020. https://doi.org/10.1109/TCAD.2020.3012859.","apa":"Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., & Schilling, C. (2020). Reachability analysis of linear hybrid systems via block decomposition. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. IEEE. https://doi.org/10.1109/TCAD.2020.3012859","ama":"Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. Reachability analysis of linear hybrid systems via block decomposition. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. 2020;39(11):4018-4029. doi:10.1109/TCAD.2020.3012859","short":"S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, C. Schilling, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 39 (2020) 4018–4029.","ieee":"S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, and C. Schilling, “Reachability analysis of linear hybrid systems via block decomposition,” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 39, no. 11. IEEE, pp. 4018–4029, 2020.","mla":"Bogomolov, Sergiy, et al. “Reachability Analysis of Linear Hybrid Systems via Block Decomposition.” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 39, no. 11, IEEE, 2020, pp. 4018–29, doi:10.1109/TCAD.2020.3012859."},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","external_id":{"isi":["000587712700072"],"arxiv":["1905.02458"]},"article_processing_charge":"No","author":[{"last_name":"Bogomolov","full_name":"Bogomolov, Sergiy","orcid":"0000-0002-0686-0365","first_name":"Sergiy","id":"369D9A44-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Marcelo","last_name":"Forets","full_name":"Forets, Marcelo"},{"first_name":"Goran","full_name":"Frehse, Goran","last_name":"Frehse"},{"first_name":"Kostiantyn","last_name":"Potomkin","full_name":"Potomkin, Kostiantyn"},{"last_name":"Schilling","full_name":"Schilling, Christian","orcid":"0000-0003-3658-1065","first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87"}],"title":"Reachability analysis of linear hybrid systems via block decomposition","project":[{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"},{"_id":"260C2330-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411"}]},{"citation":{"chicago":"Immler, Fabian, Matthias Althoff, Luis Benet, Alexandre Chapoutot, Xin Chen, Marcelo Forets, Luca Geretti, Niklas Kochdumper, David P. Sanders, and Christian Schilling. “ARCH-COMP19 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics.” In EPiC Series in Computing, 61:41–61. EasyChair Publications, 2019. https://doi.org/10.29007/m75b.","ista":"Immler F, Althoff M, Benet L, Chapoutot A, Chen X, Forets M, Geretti L, Kochdumper N, Sanders DP, Schilling C. 2019. ARCH-COMP19 Category Report: Continuous and hybrid systems with nonlinear dynamics. EPiC Series in Computing. ARCH: International Workshop on Applied Verification on Continuous and Hybrid Systems vol. 61, 41–61.","mla":"Immler, Fabian, et al. “ARCH-COMP19 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics.” EPiC Series in Computing, vol. 61, EasyChair Publications, 2019, pp. 41–61, doi:10.29007/m75b.","ama":"Immler F, Althoff M, Benet L, et al. ARCH-COMP19 Category Report: Continuous and hybrid systems with nonlinear dynamics. In: EPiC Series in Computing. Vol 61. EasyChair Publications; 2019:41-61. doi:10.29007/m75b","apa":"Immler, F., Althoff, M., Benet, L., Chapoutot, A., Chen, X., Forets, M., … Schilling, C. (2019). ARCH-COMP19 Category Report: Continuous and hybrid systems with nonlinear dynamics. In EPiC Series in Computing (Vol. 61, pp. 41–61). Montreal, Canada: EasyChair Publications. https://doi.org/10.29007/m75b","short":"F. Immler, M. Althoff, L. Benet, A. Chapoutot, X. Chen, M. Forets, L. Geretti, N. Kochdumper, D.P. Sanders, C. Schilling, in:, EPiC Series in Computing, EasyChair Publications, 2019, pp. 41–61.","ieee":"F. Immler et al., “ARCH-COMP19 Category Report: Continuous and hybrid systems with nonlinear dynamics,” in EPiC Series in Computing, Montreal, Canada, 2019, vol. 61, pp. 41–61."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","author":[{"first_name":"Fabian","last_name":"Immler","full_name":"Immler, Fabian"},{"first_name":"Matthias","last_name":"Althoff","full_name":"Althoff, Matthias"},{"first_name":"Luis","full_name":"Benet, Luis","last_name":"Benet"},{"first_name":"Alexandre","full_name":"Chapoutot, Alexandre","last_name":"Chapoutot"},{"full_name":"Chen, Xin","last_name":"Chen","first_name":"Xin"},{"first_name":"Marcelo","full_name":"Forets, Marcelo","last_name":"Forets"},{"first_name":"Luca","full_name":"Geretti, Luca","last_name":"Geretti"},{"full_name":"Kochdumper, Niklas","last_name":"Kochdumper","first_name":"Niklas"},{"first_name":"David P.","full_name":"Sanders, David P.","last_name":"Sanders"},{"last_name":"Schilling","full_name":"Schilling, Christian","orcid":"0000-0003-3658-1065","first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87"}],"title":"ARCH-COMP19 Category Report: Continuous and hybrid systems with nonlinear dynamics","oa":1,"quality_controlled":"1","publisher":"EasyChair Publications","year":"2019","has_accepted_license":"1","publication":"EPiC Series in Computing","day":"25","page":"41-61","date_created":"2020-03-08T23:00:49Z","date_published":"2019-05-25T00:00:00Z","doi":"10.29007/m75b","_id":"7576","conference":{"name":"ARCH: International Workshop on Applied Verification on Continuous and Hybrid Systems","location":"Montreal, Canada","end_date":"2019-04-15","start_date":"2019-04-15"},"type":"conference","status":"public","date_updated":"2021-01-12T08:14:17Z","ddc":["000"],"file_date_updated":"2020-07-14T12:48:00Z","department":[{"_id":"ToHe"}],"abstract":[{"text":"We present the results of a friendly competition for formal verification of continuous and hybrid systems with nonlinear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2019. In this year, 6 tools Ariadne, CORA, DynIbex, Flow*, Isabelle/HOL, and JuliaReach (in alphabetic order) participated. They are applied to solve reachability analysis problems on four benchmark problems, one of them with hybrid dynamics. We do not rank the tools based on the results, but show the current status and discover the potential advantages of different tools.","lang":"eng"}],"oa_version":"Published Version","scopus_import":1,"intvolume":" 61","month":"05","publication_status":"published","publication_identifier":{"eissn":["23987340"]},"language":[{"iso":"eng"}],"file":[{"checksum":"9138977a06fcd6a95976eb4bca875f0c","file_id":"7617","access_level":"open_access","relation":"main_file","content_type":"application/pdf","date_created":"2020-03-24T07:36:36Z","file_name":"2019_ARCH19_Immler.pdf","creator":"dernst","date_updated":"2020-07-14T12:48:00Z","file_size":1934830}],"volume":61},{"abstract":[{"text":"This report presents the results of a friendly competition for formal verification of continuous and hybrid systems with linear continuous dynamics. The friendly competition took place as part of the workshop Applied Verification for Continuous and Hybrid Systems (ARCH) in 2019. In its third edition, seven tools have been applied to solve six different benchmark problems in the category for linear continuous dynamics (in alphabetical order): CORA, CORA/SX, HyDRA, Hylaa, JuliaReach, SpaceEx, and XSpeed. This report is a snapshot of the current landscape of tools and the types of benchmarks they are particularly suited for. Due to the diversity of problems, we are not ranking tools, yet the presented results provide one of the most complete assessments of tools for the safety verification of continuous and hybrid systems with linear continuous dynamics up to this date.","lang":"eng"}],"oa_version":"Published Version","oa":1,"main_file_link":[{"open_access":"1","url":"https://easychair.org/publications/open/1gbP"}],"quality_controlled":"1","publisher":"EasyChair","intvolume":" 61","month":"05","year":"2019","publication_status":"published","publication_identifier":{"eissn":["23987340"]},"publication":"EPiC Series in Computing","language":[{"iso":"eng"}],"day":"25","page":"14-40","date_created":"2020-09-26T14:23:54Z","volume":61,"doi":"10.29007/bj1w","date_published":"2019-05-25T00:00:00Z","_id":"8570","conference":{"name":"ARCH: International Workshop on Applied Verification on Continuous and Hybrid Systems","end_date":"2019-04-15","location":"Montreal, Canada","start_date":"2019-04-15"},"type":"conference","status":"public","citation":{"ista":"Althoff M, Bak S, Forets M, Frehse G, Kochdumper N, Ray R, Schilling C, Schupp S. 2019. ARCH-COMP19 Category Report: Continuous and hybrid systems with linear continuous dynamics. EPiC Series in Computing. ARCH: International Workshop on Applied Verification on Continuous and Hybrid Systems vol. 61, 14–40.","chicago":"Althoff, Matthias, Stanley Bak, Marcelo Forets, Goran Frehse, Niklas Kochdumper, Rajarshi Ray, Christian Schilling, and Stefan Schupp. “ARCH-COMP19 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics.” In EPiC Series in Computing, 61:14–40. EasyChair, 2019. https://doi.org/10.29007/bj1w.","ieee":"M. Althoff et al., “ARCH-COMP19 Category Report: Continuous and hybrid systems with linear continuous dynamics,” in EPiC Series in Computing, Montreal, Canada, 2019, vol. 61, pp. 14–40.","short":"M. Althoff, S. Bak, M. Forets, G. Frehse, N. Kochdumper, R. Ray, C. Schilling, S. Schupp, in:, EPiC Series in Computing, EasyChair, 2019, pp. 14–40.","ama":"Althoff M, Bak S, Forets M, et al. ARCH-COMP19 Category Report: Continuous and hybrid systems with linear continuous dynamics. In: EPiC Series in Computing. Vol 61. EasyChair; 2019:14-40. doi:10.29007/bj1w","apa":"Althoff, M., Bak, S., Forets, M., Frehse, G., Kochdumper, N., Ray, R., … Schupp, S. (2019). ARCH-COMP19 Category Report: Continuous and hybrid systems with linear continuous dynamics. In EPiC Series in Computing (Vol. 61, pp. 14–40). Montreal, Canada: EasyChair. https://doi.org/10.29007/bj1w","mla":"Althoff, Matthias, et al. “ARCH-COMP19 Category Report: Continuous and Hybrid Systems with Linear Continuous Dynamics.” EPiC Series in Computing, vol. 61, EasyChair, 2019, pp. 14–40, doi:10.29007/bj1w."},"date_updated":"2021-01-12T08:20:05Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","author":[{"last_name":"Althoff","full_name":"Althoff, Matthias","first_name":"Matthias"},{"full_name":"Bak, Stanley","last_name":"Bak","first_name":"Stanley"},{"first_name":"Marcelo","last_name":"Forets","full_name":"Forets, Marcelo"},{"first_name":"Goran","full_name":"Frehse, Goran","last_name":"Frehse"},{"full_name":"Kochdumper, Niklas","last_name":"Kochdumper","first_name":"Niklas"},{"last_name":"Ray","full_name":"Ray, Rajarshi","first_name":"Rajarshi"},{"id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","first_name":"Christian","full_name":"Schilling, Christian","orcid":"0000-0003-3658-1065","last_name":"Schilling"},{"full_name":"Schupp, Stefan","last_name":"Schupp","first_name":"Stefan"}],"department":[{"_id":"ToHe"}],"title":"ARCH-COMP19 Category Report: Continuous and hybrid systems with linear continuous dynamics"},{"ddc":["000"],"date_updated":"2023-08-24T14:47:45Z","file_date_updated":"2020-07-14T12:47:17Z","department":[{"_id":"ToHe"}],"_id":"6042","status":"public","type":"conference","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"end_date":"2019-04-11","location":"Prague, Czech Republic","start_date":"2019-04-06","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"file":[{"checksum":"9998496f6fe202c0a19124b4209154c6","file_id":"6408","content_type":"application/pdf","relation":"main_file","access_level":"open_access","file_name":"2019_LNCS_Christakis.pdf","date_created":"2019-05-10T14:16:05Z","file_size":773083,"date_updated":"2020-07-14T12:47:17Z","creator":"dernst"}],"language":[{"iso":"eng"}],"publication_status":"published","volume":11427,"ec_funded":1,"oa_version":"Published Version","abstract":[{"text":"Static program analyzers are increasingly effective in checking correctness properties of programs and reporting any errors found, often in the form of error traces. However, developers still spend a significant amount of time on debugging. This involves processing long error traces in an effort to localize a bug to a relatively small part of the program and to identify its cause. In this paper, we present a technique for automated fault localization that, given a program and an error trace, efficiently narrows down the cause of the error to a few statements. These statements are then ranked in terms of their suspiciousness. Our technique relies only on the semantics of the given program and does not require any test cases or user guidance. In experiments on a set of C benchmarks, we show that our technique is effective in quickly isolating the cause of error while out-performing other state-of-the-art fault-localization techniques.","lang":"eng"}],"month":"04","intvolume":" 11427","alternative_title":["LNCS"],"scopus_import":"1","user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"mla":"Christakis, Maria, et al. “Semantic Fault Localization and Suspiciousness Ranking.” 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , vol. 11427, Springer Nature, 2019, pp. 226–43, doi:10.1007/978-3-030-17462-0_13.","apa":"Christakis, M., Heizmann, M., Mansur, M. N., Schilling, C., & Wüstholz, V. (2019). Semantic fault localization and suspiciousness ranking. In 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (Vol. 11427, pp. 226–243). Prague, Czech Republic: Springer Nature. https://doi.org/10.1007/978-3-030-17462-0_13","ama":"Christakis M, Heizmann M, Mansur MN, Schilling C, Wüstholz V. Semantic fault localization and suspiciousness ranking. In: 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems . Vol 11427. Springer Nature; 2019:226-243. doi:10.1007/978-3-030-17462-0_13","ieee":"M. Christakis, M. Heizmann, M. N. Mansur, C. Schilling, and V. Wüstholz, “Semantic fault localization and suspiciousness ranking,” in 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , Prague, Czech Republic, 2019, vol. 11427, pp. 226–243.","short":"M. Christakis, M. Heizmann, M.N. Mansur, C. Schilling, V. Wüstholz, in:, 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , Springer Nature, 2019, pp. 226–243.","chicago":"Christakis, Maria, Matthias Heizmann, Muhammad Numair Mansur, Christian Schilling, and Valentin Wüstholz. “Semantic Fault Localization and Suspiciousness Ranking.” In 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , 11427:226–43. Springer Nature, 2019. https://doi.org/10.1007/978-3-030-17462-0_13.","ista":"Christakis M, Heizmann M, Mansur MN, Schilling C, Wüstholz V. 2019. Semantic fault localization and suspiciousness ranking. 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems . TACAS: Tools and Algorithms for the Construction and Analysis of Systems, LNCS, vol. 11427, 226–243."},"title":"Semantic fault localization and suspiciousness ranking","author":[{"full_name":"Christakis, Maria","last_name":"Christakis","first_name":"Maria"},{"full_name":"Heizmann, Matthias","last_name":"Heizmann","first_name":"Matthias"},{"full_name":"Mansur, Muhammad Numair","last_name":"Mansur","first_name":"Muhammad Numair"},{"first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","last_name":"Schilling","full_name":"Schilling, Christian","orcid":"0000-0003-3658-1065"},{"full_name":"Wüstholz, Valentin","last_name":"Wüstholz","first_name":"Valentin"}],"article_processing_charge":"No","external_id":{"isi":["000681166500013"]},"project":[{"name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411","call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425"},{"name":"The Wittgenstein Prize","grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"}],"day":"04","publication":"25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems ","isi":1,"has_accepted_license":"1","year":"2019","doi":"10.1007/978-3-030-17462-0_13","date_published":"2019-04-04T00:00:00Z","date_created":"2019-02-18T16:44:06Z","page":"226-243","quality_controlled":"1","publisher":"Springer Nature","oa":1},{"oa":1,"publisher":"ACM","quality_controlled":"1","date_created":"2019-02-18T14:43:28Z","doi":"10.1145/3302504.3311804","date_published":"2019-04-16T00:00:00Z","page":"39-44","publication":"Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control","day":"16","year":"2019","has_accepted_license":"1","isi":1,"project":[{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"call_identifier":"H2020","_id":"260C2330-B435-11E9-9278-68D0E5697425","grant_number":"754411","name":"ISTplus - Postdoctoral Fellowships"}],"title":"JuliaReach: A toolbox for set-based reachability","article_processing_charge":"No","external_id":{"arxiv":["1901.10736"],"isi":["000516713900005"]},"author":[{"last_name":"Bogomolov","full_name":"Bogomolov, Sergiy","orcid":"0000-0002-0686-0365","first_name":"Sergiy","id":"369D9A44-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Forets","full_name":"Forets, Marcelo","first_name":"Marcelo"},{"full_name":"Frehse, Goran","last_name":"Frehse","first_name":"Goran"},{"last_name":"Potomkin","full_name":"Potomkin, Kostiantyn","first_name":"Kostiantyn"},{"last_name":"Schilling","orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","first_name":"Christian"}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"chicago":"Bogomolov, Sergiy, Marcelo Forets, Goran Frehse, Kostiantyn Potomkin, and Christian Schilling. “JuliaReach: A Toolbox for Set-Based Reachability.” In Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control, 22:39–44. ACM, 2019. https://doi.org/10.1145/3302504.3311804.","ista":"Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. 2019. JuliaReach: A toolbox for set-based reachability. Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control. HSCC: Hybrid Systems Computation and Control vol. 22, 39–44.","mla":"Bogomolov, Sergiy, et al. “JuliaReach: A Toolbox for Set-Based Reachability.” Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control, vol. 22, ACM, 2019, pp. 39–44, doi:10.1145/3302504.3311804.","short":"S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, C. Schilling, in:, Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control, ACM, 2019, pp. 39–44.","ieee":"S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, and C. Schilling, “JuliaReach: A toolbox for set-based reachability,” in Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control, Montreal, QC, Canada, 2019, vol. 22, pp. 39–44.","ama":"Bogomolov S, Forets M, Frehse G, Potomkin K, Schilling C. JuliaReach: A toolbox for set-based reachability. In: Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control. Vol 22. ACM; 2019:39-44. doi:10.1145/3302504.3311804","apa":"Bogomolov, S., Forets, M., Frehse, G., Potomkin, K., & Schilling, C. (2019). JuliaReach: A toolbox for set-based reachability. In Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control (Vol. 22, pp. 39–44). Montreal, QC, Canada: ACM. https://doi.org/10.1145/3302504.3311804"},"intvolume":" 22","month":"04","scopus_import":"1","oa_version":"Submitted Version","abstract":[{"text":"We present JuliaReach, a toolbox for set-based reachability analysis of dynamical systems. JuliaReach consists of two main packages: Reachability, containing implementations of reachability algorithms for continuous and hybrid systems, and LazySets, a standalone library that implements state-of-the-art algorithms for calculus with convex sets. The library offers both concrete and lazy set representations, where the latter stands for the ability to delay set computations until they are needed. The choice of the programming language Julia and the accompanying documentation of our toolbox allow researchers to easily translate set-based algorithms from mathematics to software in a platform-independent way, while achieving runtime performance that is comparable to statically compiled languages. Combining lazy operations in high dimensions and explicit computations in low dimensions, JuliaReach can be applied to solve complex, large-scale problems.","lang":"eng"}],"ec_funded":1,"volume":22,"language":[{"iso":"eng"}],"file":[{"checksum":"28ed56439aea5991c3122d4730fd828f","file_id":"6067","content_type":"application/pdf","relation":"main_file","access_level":"open_access","file_name":"hscc19.pdf","date_created":"2019-03-05T09:27:18Z","file_size":3784414,"date_updated":"2020-07-14T12:47:17Z","creator":"cschilli"}],"publication_status":"published","publication_identifier":{"isbn":["9781450362825"]},"keyword":["reachability analysis","hybrid systems","lazy computation"],"status":"public","conference":{"start_date":"2019-04-16","end_date":"2019-04-18","location":"Montreal, QC, Canada","name":"HSCC: Hybrid Systems Computation and Control"},"type":"conference","_id":"6035","file_date_updated":"2020-07-14T12:47:17Z","department":[{"_id":"ToHe"}],"ddc":["000"],"date_updated":"2023-08-24T14:47:21Z"},{"intvolume":" 11561","month":"07","scopus_import":"1","alternative_title":["LNCS"],"oa_version":"Published Version","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."}],"ec_funded":1,"volume":11561,"language":[{"iso":"eng"}],"file":[{"file_size":674795,"date_updated":"2020-07-14T12:47:32Z","creator":"dernst","file_name":"2019_CAV_GarciaSoto.pdf","date_created":"2019-08-14T11:05:30Z","content_type":"application/pdf","relation":"main_file","access_level":"open_access","checksum":"1f1d61b83a151031745ef70a501da3d6","file_id":"6817"}],"publication_status":"published","publication_identifier":{"isbn":["9783030255398"],"issn":["0302-9743"]},"keyword":["Synthesis","Linear hybrid automaton","Membership"],"status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"conference":{"start_date":"2019-07-15","location":"New York City, NY, USA","end_date":"2019-07-18","name":"CAV: Computer-Aided Verification"},"type":"conference","_id":"6493","department":[{"_id":"ToHe"}],"file_date_updated":"2020-07-14T12:47:32Z","ddc":["000"],"date_updated":"2023-08-25T10:40:41Z","oa":1,"quality_controlled":"1","publisher":"Springer","date_created":"2019-05-27T07:09:53Z","date_published":"2019-07-12T00:00:00Z","doi":"10.1007/978-3-030-25540-4_16","page":"297-314","publication":"31st International Conference on Computer-Aided Verification","day":"12","year":"2019","isi":1,"has_accepted_license":"1","project":[{"name":"ISTplus - Postdoctoral Fellowships","grant_number":"754411","_id":"260C2330-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"},{"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"}],"title":"Membership-based synthesis of linear hybrid automata","external_id":{"isi":["000491468000016"]},"article_processing_charge":"No","author":[{"first_name":"Miriam","id":"4B3207F6-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0003−2936−5719","full_name":"Garcia Soto, Miriam","last_name":"Garcia Soto"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","last_name":"Schilling","orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian"},{"full_name":"Zeleznik, Luka","last_name":"Zeleznik","id":"3ADCA2E4-F248-11E8-B48F-1D18A9856A87","first_name":"Luka"}],"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","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.","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.","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.","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","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.","short":"M. Garcia Soto, T.A. Henzinger, C. Schilling, L. Zeleznik, in:, 31st International Conference on Computer-Aided Verification, Springer, 2019, pp. 297–314."}},{"_id":"1134","article_number":"7587948","type":"conference","conference":{"name":"CCA: Control Applications ","end_date":"2016-09-22","location":"Buenos Aires, Argentina ","start_date":"2016-09-19"},"status":"public","citation":{"mla":"Duggirala, Parasara, et al. “Tutorial: Software Tools for Hybrid Systems Verification Transformation and Synthesis C2E2 HyST and TuLiP.” 2016 IEEE Conference on Control Applications, 7587948, IEEE, 2016, doi:10.1109/CCA.2016.7587948.","ieee":"P. Duggirala et al., “Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP,” in 2016 IEEE Conference on Control Applications, Buenos Aires, Argentina , 2016.","short":"P. Duggirala, C. Fan, M. Potok, B. Qi, S. Mitra, M. Viswanathan, S. Bak, S. Bogomolov, T. Johnson, L. Nguyen, C. Schilling, A. Sogokon, H. Tran, W. Xiang, in:, 2016 IEEE Conference on Control Applications, IEEE, 2016.","apa":"Duggirala, P., Fan, C., Potok, M., Qi, B., Mitra, S., Viswanathan, M., … Xiang, W. (2016). Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP. In 2016 IEEE Conference on Control Applications. Buenos Aires, Argentina : IEEE. https://doi.org/10.1109/CCA.2016.7587948","ama":"Duggirala P, Fan C, Potok M, et al. Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP. In: 2016 IEEE Conference on Control Applications. IEEE; 2016. doi:10.1109/CCA.2016.7587948","chicago":"Duggirala, Parasara, Chuchu Fan, Matthew Potok, Bolun Qi, Sayan Mitra, Mahesh Viswanathan, Stanley Bak, et al. “Tutorial: Software Tools for Hybrid Systems Verification Transformation and Synthesis C2E2 HyST and TuLiP.” In 2016 IEEE Conference on Control Applications. IEEE, 2016. https://doi.org/10.1109/CCA.2016.7587948.","ista":"Duggirala P, Fan C, Potok M, Qi B, Mitra S, Viswanathan M, Bak S, Bogomolov S, Johnson T, Nguyen L, Schilling C, Sogokon A, Tran H, Xiang W. 2016. Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP. 2016 IEEE Conference on Control Applications. CCA: Control Applications , 7587948."},"date_updated":"2021-01-12T06:48:32Z","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Duggirala, Parasara","last_name":"Duggirala","first_name":"Parasara"},{"full_name":"Fan, Chuchu","last_name":"Fan","first_name":"Chuchu"},{"first_name":"Matthew","last_name":"Potok","full_name":"Potok, Matthew"},{"first_name":"Bolun","last_name":"Qi","full_name":"Qi, Bolun"},{"last_name":"Mitra","full_name":"Mitra, Sayan","first_name":"Sayan"},{"last_name":"Viswanathan","full_name":"Viswanathan, Mahesh","first_name":"Mahesh"},{"last_name":"Bak","full_name":"Bak, Stanley","first_name":"Stanley"},{"full_name":"Bogomolov, Sergiy","orcid":"0000-0002-0686-0365","last_name":"Bogomolov","first_name":"Sergiy","id":"369D9A44-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Johnson, Taylor","last_name":"Johnson","first_name":"Taylor"},{"first_name":"Luan","full_name":"Nguyen, Luan","last_name":"Nguyen"},{"id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","first_name":"Christian","last_name":"Schilling","orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian"},{"first_name":"Andrew","full_name":"Sogokon, Andrew","last_name":"Sogokon"},{"first_name":"Hoang","last_name":"Tran","full_name":"Tran, Hoang"},{"full_name":"Xiang, Weiming","last_name":"Xiang","first_name":"Weiming"}],"publist_id":"6224","department":[{"_id":"ToHe"}],"title":"Tutorial: Software tools for hybrid systems verification transformation and synthesis C2E2 HyST and TuLiP","abstract":[{"text":"Hybrid systems have both continuous and discrete dynamics and are useful for modeling a variety of control systems, from air traffic control protocols to robotic maneuvers and beyond. Recently, numerous powerful and scalable tools for analyzing hybrid systems have emerged. Several of these tools implement automated formal methods for mathematically proving a system meets a specification. This tutorial session will present three recent hybrid systems tools: C2E2, HyST, and TuLiP. C2E2 is a simulated-based verification tool for hybrid systems, and uses validated numerical solvers and bloating of simulation traces to verify systems meet specifications. HyST is a hybrid systems model transformation and translation tool, and uses a canonical intermediate representation to support most of the recent verification tools, as well as automated sound abstractions that simplify verification of a given hybrid system. TuLiP is a controller synthesis tool for hybrid systems, where given a temporal logic specification to be satisfied for a system (plant) model, TuLiP will find a controller that meets a given specification. © 2016 IEEE.","lang":"eng"}],"oa_version":"None","scopus_import":1,"publisher":"IEEE","quality_controlled":"1","month":"10","year":"2016","publication_status":"published","day":"10","language":[{"iso":"eng"}],"publication":"2016 IEEE Conference on Control Applications","doi":"10.1109/CCA.2016.7587948","date_published":"2016-10-10T00:00:00Z","date_created":"2018-12-11T11:50:20Z"},{"_id":"1227","type":"conference","conference":{"end_date":"2016-10-21","location":"Grenoble, France","start_date":"2016-10-20","name":"HSB: Hybrid Systems Biology"},"status":"public","pubrep_id":"781","date_updated":"2021-01-12T06:49:13Z","ddc":["005"],"file_date_updated":"2020-07-14T12:44:39Z","department":[{"_id":"ToHe"}],"abstract":[{"lang":"eng","text":"Many biological systems can be modeled as multiaffine hybrid systems. Due to the nonlinearity of multiaffine systems, it is difficult to verify their properties of interest directly. A common strategy to tackle this problem is to construct and analyze a discrete overapproximation of the original system. However, the conservativeness of a discrete abstraction significantly determines the level of confidence we can have in the properties of the original system. In this paper, in order to reduce the conservativeness of a discrete abstraction, we propose a new method based on a sufficient and necessary decision condition for computing discrete transitions between states in the abstract system. We assume the state space partition of a multiaffine system to be based on a set of multivariate polynomials. Hence, a rectangular partition defined in terms of polynomials of the form (xi − c) is just a simple case of multivariate polynomial partition, and the new decision condition applies naturally. We analyze and demonstrate the improvement of our method over the existing methods using some examples."}],"oa_version":"Submitted Version","scopus_import":1,"alternative_title":["LNCS"],"month":"09","intvolume":" 9957","publication_status":"published","file":[{"access_level":"open_access","relation":"main_file","content_type":"application/pdf","checksum":"994e164b558c47bacf8dc066dd27c8fc","file_id":"4840","creator":"system","date_updated":"2020-07-14T12:44:39Z","file_size":683955,"date_created":"2018-12-12T10:10:49Z","file_name":"IST-2017-781-v1+1_main.pdf"}],"language":[{"iso":"eng"}],"volume":9957,"project":[{"name":"The Wittgenstein Prize","grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"citation":{"mla":"Kong, Hui, et al. Discrete Abstraction of Multiaffine Systems. Vol. 9957, Springer, 2016, pp. 128–44, doi:10.1007/978-3-319-47151-8_9.","apa":"Kong, H., Bartocci, E., Bogomolov, S., Grosu, R., Henzinger, T. A., Jiang, Y., & Schilling, C. (2016). Discrete abstraction of multiaffine systems (Vol. 9957, pp. 128–144). Presented at the HSB: Hybrid Systems Biology, Grenoble, France: Springer. https://doi.org/10.1007/978-3-319-47151-8_9","ama":"Kong H, Bartocci E, Bogomolov S, et al. Discrete abstraction of multiaffine systems. In: Vol 9957. Springer; 2016:128-144. doi:10.1007/978-3-319-47151-8_9","short":"H. Kong, E. Bartocci, S. Bogomolov, R. Grosu, T.A. Henzinger, Y. Jiang, C. Schilling, in:, Springer, 2016, pp. 128–144.","ieee":"H. Kong et al., “Discrete abstraction of multiaffine systems,” presented at the HSB: Hybrid Systems Biology, Grenoble, France, 2016, vol. 9957, pp. 128–144.","chicago":"Kong, Hui, Ezio Bartocci, Sergiy Bogomolov, Radu Grosu, Thomas A Henzinger, Yu Jiang, and Christian Schilling. “Discrete Abstraction of Multiaffine Systems,” 9957:128–44. Springer, 2016. https://doi.org/10.1007/978-3-319-47151-8_9.","ista":"Kong H, Bartocci E, Bogomolov S, Grosu R, Henzinger TA, Jiang Y, Schilling C. 2016. Discrete abstraction of multiaffine systems. HSB: Hybrid Systems Biology, LNCS, vol. 9957, 128–144."},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","author":[{"full_name":"Kong, Hui","orcid":"0000-0002-3066-6941","last_name":"Kong","first_name":"Hui","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ezio","last_name":"Bartocci","full_name":"Bartocci, Ezio"},{"id":"369D9A44-F248-11E8-B48F-1D18A9856A87","first_name":"Sergiy","full_name":"Bogomolov, Sergiy","orcid":"0000-0002-0686-0365","last_name":"Bogomolov"},{"full_name":"Grosu, Radu","last_name":"Grosu","first_name":"Radu"},{"last_name":"Henzinger","orcid":"0000−0002−2985−7724","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"first_name":"Yu","last_name":"Jiang","full_name":"Jiang, Yu"},{"first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","last_name":"Schilling","orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian"}],"publist_id":"6107","title":"Discrete abstraction of multiaffine systems","acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grants S11402-N23, S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award).","publisher":"Springer","quality_controlled":"1","oa":1,"has_accepted_license":"1","year":"2016","day":"25","page":"128 - 144","date_published":"2016-09-25T00:00:00Z","doi":"10.1007/978-3-319-47151-8_9","date_created":"2018-12-11T11:50:49Z"},{"citation":{"mla":"Nguyen, Luan, et al. “Poster: HyRG: A Random Generation Tool for Affine Hybrid Automata.” HSCC: Hybrid Systems - Computation and Control, Springer, 2015, pp. 289–90, doi:10.1145/2728606.2728650.","ama":"Nguyen L, Schilling C, Bogomolov S, Johnson T. Poster: HyRG: A Random Generation Tool for Affine Hybrid Automata. Springer; 2015:289-290. doi:10.1145/2728606.2728650","apa":"Nguyen, L., Schilling, C., Bogomolov, S., & Johnson, T. (2015). Poster: HyRG: A random generation tool for affine hybrid automata. HSCC: Hybrid Systems - Computation and Control (pp. 289–290). Springer. https://doi.org/10.1145/2728606.2728650","short":"L. Nguyen, C. Schilling, S. Bogomolov, T. Johnson, Poster: HyRG: A Random Generation Tool for Affine Hybrid Automata, Springer, 2015.","ieee":"L. Nguyen, C. Schilling, S. Bogomolov, and T. Johnson, Poster: HyRG: A random generation tool for affine hybrid automata. Springer, 2015, pp. 289–290.","chicago":"Nguyen, Luan, Christian Schilling, Sergiy Bogomolov, and Taylor Johnson. Poster: HyRG: A Random Generation Tool for Affine Hybrid Automata. HSCC: Hybrid Systems - Computation and Control. Springer, 2015. https://doi.org/10.1145/2728606.2728650.","ista":"Nguyen L, Schilling C, Bogomolov S, Johnson T. 2015. Poster: HyRG: A random generation tool for affine hybrid automata, Springer,p."},"date_updated":"2019-04-26T07:22:03Z","extern":1,"author":[{"first_name":"Luan","last_name":"Nguyen","full_name":"Nguyen, Luan V"},{"first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0003-3658-1065","full_name":"Christian Schilling","last_name":"Schilling"},{"full_name":"Sergiy Bogomolov","orcid":"0000-0002-0686-0365","last_name":"Bogomolov","id":"369D9A44-F248-11E8-B48F-1D18A9856A87","first_name":"Sergiy"},{"full_name":"Johnson, Taylor T","last_name":"Johnson","first_name":"Taylor"}],"publist_id":"5678","title":"Poster: HyRG: A random generation tool for affine hybrid automata","_id":"1500","type":"conference_poster","status":"public","publication_status":"published","year":"2015","day":"14","publication":"HSCC: Hybrid Systems - Computation and Control","page":"289 - 290","date_published":"2015-04-14T00:00:00Z","doi":"10.1145/2728606.2728650","date_created":"2018-12-11T11:52:23Z","abstract":[{"text":"In this poster, we present methods for randomly generating hybrid automata with affine differential equations, invariants, guards, and assignments. Selecting an arbitrary affine function from the set of all affine functions results in a low likelihood of generating hybrid automata with diverse and interesting behaviors, as there are an uncountable number of elements in the set of all affine functions. Instead, we partition the set of all affine functions into potentially interesting classes and randomly select elements from these classes. For example, we partition the set of all affine differential equations by using restrictions on eigenvalues such as those that yield stable, unstable, etc. equilibrium points. We partition the components describing discrete behavior (guards, assignments, and invariants) to allow either time-dependent or state-dependent switching, and in particular provide the ability to generate subclasses of piecewise-affine hybrid automata. Our preliminary experimental results with a prototype tool called HyRG (Hybrid Random Generator) illustrate the feasibility of this generation method to automatically create standard hybrid automaton examples like the bouncing ball and thermostat.","lang":"eng"}],"quality_controlled":0,"alternative_title":["18th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2015"],"publisher":"Springer","month":"04"},{"publication_status":"published","language":[{"iso":"eng"}],"file":[{"date_updated":"2020-07-14T12:45:05Z","file_size":1053207,"creator":"dernst","date_created":"2020-05-15T08:43:19Z","file_name":"2015_LNCS_Bogomolov.pdf","content_type":"application/pdf","access_level":"open_access","relation":"main_file","checksum":"3aab260f3f34641d622030ba22645b3e","file_id":"7851"}],"ec_funded":1,"volume":9434,"abstract":[{"text":"Multiaffine hybrid automata (MHA) represent a powerful formalism to model complex dynamical systems. This formalism is particularly suited for the representation of biological systems which often exhibit highly non-linear behavior. In this paper, we consider the problem of parameter identification for MHA. We present an abstraction of MHA based on linear hybrid automata, which can be analyzed by the SpaceEx model checker. This abstraction enables a precise handling of time-dependent properties. We demonstrate the potential of our approach on a model of a genetic regulatory network and a myocyte model.","lang":"eng"}],"oa_version":"Submitted Version","scopus_import":1,"alternative_title":["LNCS"],"intvolume":" 9434","month":"11","date_updated":"2021-01-12T06:51:56Z","ddc":["000"],"department":[{"_id":"ToHe"}],"file_date_updated":"2020-07-14T12:45:05Z","_id":"1605","conference":{"start_date":"2015-11-17","location":"Haifa, Israel","end_date":"2015-11-19","name":"HVC: Haifa Verification Conference"},"type":"conference","status":"public","year":"2015","has_accepted_license":"1","day":"28","page":"19 - 35","date_created":"2018-12-11T11:52:59Z","date_published":"2015-11-28T00:00:00Z","doi":"10.1007/978-3-319-26287-1_2","acknowledgement":"This work was partly supported by the European Research Council (ERC) under grant 267989 (QUAREM), by the Austrian Science Fund (FWF) under grants S11402-N23, S11405-N23 and S11412-N23 (RiSE/SHiNE) and Z211-N23 (Wittgenstein Award), and by the German Research Foundation (DFG) as part of the Transregional Collaborative Research Center “Automatic Verification and Analysis of Complex Systems” (SFB/TR 14 AVACS, http://www.avacs.org/).","oa":1,"publisher":"Springer","quality_controlled":"1","citation":{"chicago":"Bogomolov, Sergiy, Christian Schilling, Ezio Bartocci, Grégory Batt, Hui Kong, and Radu Grosu. “Abstraction-Based Parameter Synthesis for Multiaffine Systems,” 9434:19–35. Springer, 2015. https://doi.org/10.1007/978-3-319-26287-1_2.","ista":"Bogomolov S, Schilling C, Bartocci E, Batt G, Kong H, Grosu R. 2015. Abstraction-based parameter synthesis for multiaffine systems. HVC: Haifa Verification Conference, LNCS, vol. 9434, 19–35.","mla":"Bogomolov, Sergiy, et al. Abstraction-Based Parameter Synthesis for Multiaffine Systems. Vol. 9434, Springer, 2015, pp. 19–35, doi:10.1007/978-3-319-26287-1_2.","ieee":"S. Bogomolov, C. Schilling, E. Bartocci, G. Batt, H. Kong, and R. Grosu, “Abstraction-based parameter synthesis for multiaffine systems,” presented at the HVC: Haifa Verification Conference, Haifa, Israel, 2015, vol. 9434, pp. 19–35.","short":"S. Bogomolov, C. Schilling, E. Bartocci, G. Batt, H. Kong, R. Grosu, in:, Springer, 2015, pp. 19–35.","apa":"Bogomolov, S., Schilling, C., Bartocci, E., Batt, G., Kong, H., & Grosu, R. (2015). Abstraction-based parameter synthesis for multiaffine systems (Vol. 9434, pp. 19–35). Presented at the HVC: Haifa Verification Conference, Haifa, Israel: Springer. https://doi.org/10.1007/978-3-319-26287-1_2","ama":"Bogomolov S, Schilling C, Bartocci E, Batt G, Kong H, Grosu R. Abstraction-based parameter synthesis for multiaffine systems. In: Vol 9434. Springer; 2015:19-35. doi:10.1007/978-3-319-26287-1_2"},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","publist_id":"5561","author":[{"last_name":"Bogomolov","full_name":"Bogomolov, Sergiy","orcid":"0000-0002-0686-0365","first_name":"Sergiy","id":"369D9A44-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Schilling","full_name":"Schilling, Christian","orcid":"0000-0003-3658-1065","first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Ezio","full_name":"Bartocci, Ezio","last_name":"Bartocci"},{"full_name":"Batt, Grégory","last_name":"Batt","first_name":"Grégory"},{"full_name":"Kong, Hui","orcid":"0000-0002-3066-6941","last_name":"Kong","id":"3BDE25AA-F248-11E8-B48F-1D18A9856A87","first_name":"Hui"},{"first_name":"Radu","full_name":"Grosu, Radu","last_name":"Grosu"}],"title":"Abstraction-based parameter synthesis for multiaffine systems","project":[{"call_identifier":"FP7","_id":"25EE3708-B435-11E9-9278-68D0E5697425","grant_number":"267989","name":"Quantitative Reactive Modeling"},{"_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize","grant_number":"Z211"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}]}]