[{"oa_version":"None","month":"10","publication":"20th International Symposium on Automated Technology for Verification and Analysis","conference":{"name":"ATVA: Automated Technology for Verification and Analysis","start_date":"2022-10-25","end_date":"2022-10-28","location":"Virtual"},"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["9783031199912"],"eissn":["1611-3349"],"issn":["0302-9743"],"eisbn":["9783031199929"]},"date_published":"2022-10-21T00:00:00Z","type":"conference","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","status":"public","publication_status":"published","department":[{"_id":"KrCh"}],"date_created":"2023-01-12T12:11:07Z","article_processing_charge":"No","title":"PET – A partial exploration tool for probabilistic verification","alternative_title":["LNCS"],"intvolume":"     13505","_id":"12170","scopus_import":"1","author":[{"id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","last_name":"Meggendorfer","first_name":"Tobias","full_name":"Meggendorfer, Tobias","orcid":"0000-0002-1712-2165"}],"publisher":"Springer Nature","page":"320-326","quality_controlled":"1","doi":"10.1007/978-3-031-19992-9_20","day":"21","abstract":[{"lang":"eng","text":"We present PET, a specialized and highly optimized framework for partial exploration on probabilistic systems. Over the last decade, several significant advances in the analysis of Markov decision processes employed partial exploration. In a nutshell, this idea allows to focus computation on specific parts of the system, guided by heuristics, while maintaining correctness. In particular, only relevant parts of the system are constructed on demand, which in turn potentially allows to omit constructing large parts of the system. Depending on the model, this leads to dramatic speed-ups, in extreme cases even up to an arbitrary factor. PET unifies several previous implementations and provides a flexible framework to easily implement partial exploration for many further problems. Our experimental evaluation shows significant improvements compared to the previous implementations while vastly reducing the overhead required to add support for additional properties."}],"date_updated":"2023-09-05T15:11:51Z","year":"2022","citation":{"chicago":"Meggendorfer, Tobias. “PET – A Partial Exploration Tool for Probabilistic Verification.” In <i>20th International Symposium on Automated Technology for Verification and Analysis</i>, 13505:320–26. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-031-19992-9_20\">https://doi.org/10.1007/978-3-031-19992-9_20</a>.","ieee":"T. Meggendorfer, “PET – A partial exploration tool for probabilistic verification,” in <i>20th International Symposium on Automated Technology for Verification and Analysis</i>, Virtual, 2022, vol. 13505, pp. 320–326.","ama":"Meggendorfer T. PET – A partial exploration tool for probabilistic verification. In: <i>20th International Symposium on Automated Technology for Verification and Analysis</i>. Vol 13505. Springer Nature; 2022:320-326. doi:<a href=\"https://doi.org/10.1007/978-3-031-19992-9_20\">10.1007/978-3-031-19992-9_20</a>","apa":"Meggendorfer, T. (2022). PET – A partial exploration tool for probabilistic verification. In <i>20th International Symposium on Automated Technology for Verification and Analysis</i> (Vol. 13505, pp. 320–326). Virtual: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-19992-9_20\">https://doi.org/10.1007/978-3-031-19992-9_20</a>","ista":"Meggendorfer T. 2022. PET – A partial exploration tool for probabilistic verification. 20th International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 13505, 320–326.","mla":"Meggendorfer, Tobias. “PET – A Partial Exploration Tool for Probabilistic Verification.” <i>20th International Symposium on Automated Technology for Verification and Analysis</i>, vol. 13505, Springer Nature, 2022, pp. 320–26, doi:<a href=\"https://doi.org/10.1007/978-3-031-19992-9_20\">10.1007/978-3-031-19992-9_20</a>.","short":"T. Meggendorfer, in:, 20th International Symposium on Automated Technology for Verification and Analysis, Springer Nature, 2022, pp. 320–326."},"acknowledgement":"We thank Pranav Ashok and Maximilian Weininger for their contributions to spiritual predecessors of PET as well as motivating the initial development of this tool.","volume":13505},{"volume":13505,"acknowledgement":"This work was supported in part by the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement no. 847635, by the ERC-2020-AdG 101020093, by DIREC - Digital Research Centre Denmark, and by the Villum Investigator Grant S4OS.","date_updated":"2023-02-13T09:27:55Z","year":"2022","citation":{"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.","short":"M. Garcia Soto, T.A. Henzinger, C. Schilling, in:, 20th International Symposium on Automated Technology for Verification and Analysis, Springer Nature, 2022, pp. 337–353.","mla":"Garcia Soto, Miriam, et al. “Synthesis of Parametric Hybrid Automata from Time Series.” <i>20th International Symposium on Automated Technology for Verification and Analysis</i>, vol. 13505, Springer Nature, 2022, pp. 337–53, doi:<a href=\"https://doi.org/10.1007/978-3-031-19992-9_22\">10.1007/978-3-031-19992-9_22</a>.","ieee":"M. Garcia Soto, T. A. Henzinger, and C. Schilling, “Synthesis of parametric hybrid automata from time series,” in <i>20th International Symposium on Automated Technology for Verification and Analysis</i>, Virtual, 2022, vol. 13505, pp. 337–353.","chicago":"Garcia Soto, Miriam, Thomas A Henzinger, and Christian Schilling. “Synthesis of Parametric Hybrid Automata from Time Series.” In <i>20th International Symposium on Automated Technology for Verification and Analysis</i>, 13505:337–53. Springer Nature, 2022. <a href=\"https://doi.org/10.1007/978-3-031-19992-9_22\">https://doi.org/10.1007/978-3-031-19992-9_22</a>.","ama":"Garcia Soto M, Henzinger TA, Schilling C. Synthesis of parametric hybrid automata from time series. In: <i>20th International Symposium on Automated Technology for Verification and Analysis</i>. Vol 13505. Springer Nature; 2022:337-353. doi:<a href=\"https://doi.org/10.1007/978-3-031-19992-9_22\">10.1007/978-3-031-19992-9_22</a>","apa":"Garcia Soto, M., Henzinger, T. A., &#38; Schilling, C. (2022). Synthesis of parametric hybrid automata from time series. In <i>20th International Symposium on Automated Technology for Verification and Analysis</i> (Vol. 13505, pp. 337–353). Virtual: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-19992-9_22\">https://doi.org/10.1007/978-3-031-19992-9_22</a>"},"external_id":{"arxiv":["2208.06383"]},"doi":"10.1007/978-3-031-19992-9_22","arxiv":1,"day":"21","abstract":[{"lang":"eng","text":"We propose an algorithmic approach for synthesizing linear hybrid automata from time-series data. Unlike existing approaches, our approach provides a whole family of models with the same discrete structure but different dynamics. Each model in the family is guaranteed to capture the input data up to a precision error ε, in the following sense: For each time series, the model contains an execution that is ε-close to the data points. Our construction allows to effectively choose a model from this family with minimal precision error ε. We demonstrate the algorithm’s efficiency and its ability to find precise models in two case studies."}],"page":"337-353","quality_controlled":"1","ec_funded":1,"publisher":"Springer Nature","_id":"12171","scopus_import":"1","author":[{"orcid":"0000-0003-2936-5719","full_name":"Garcia Soto, Miriam","first_name":"Miriam","last_name":"Garcia Soto","id":"4B3207F6-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","first_name":"Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0003-3658-1065","full_name":"Schilling, Christian","first_name":"Christian","last_name":"Schilling","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87"}],"publication_status":"published","article_processing_charge":"No","department":[{"_id":"ToHe"}],"date_created":"2023-01-12T12:11:16Z","alternative_title":["LNCS"],"title":"Synthesis of parametric hybrid automata from time series","intvolume":"     13505","main_file_link":[{"open_access":"1","url":"https://doi.org/10.48550/arXiv.2208.06383"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","date_published":"2022-10-21T00:00:00Z","type":"conference","publication_identifier":{"isbn":["9783031199912"],"eisbn":["9783031199929"],"issn":["0302-9743"],"eissn":["1611-3349"]},"oa":1,"language":[{"iso":"eng"}],"conference":{"name":"ATVA: Automated Technology for Verification and Analysis","start_date":"2022-10-25","end_date":"2022-10-28","location":"Virtual"},"publication":"20th International Symposium on Automated Technology for Verification and Analysis","oa_version":"Preprint","project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"month":"10"}]