[{"OA_place":"publisher","related_material":{"record":[{"relation":"research_data","status":"public","id":"19769"}]},"acknowledgement":"This work was supported by the DFG through the Cluster of Excellence EXC 2050/1 (CeTI, project ID 390696704, as part of Germany’s Excellence Strategy) and the TRR 248 (see perspicuous-computing.science, project ID 389792660), by the European Union’s Horizon 2020 research and innovation programme under Marie Skłodowska-Curie grant agreements 101008233 (MISSION), 101034413 (IST-BRIDGE), and 101067199 (ProSVED), by the EU under NextGenerationEU projects D53D23008400006 (Smartitude) under MUR PRIN 2022 and PE00000014 (SERICS) under MUR PNRR, by the Interreg North Sea project STORM_SAFE, and by NWO VIDI grant VI.Vidi.223.110 (TruSTy).","author":[{"last_name":"Budde","first_name":"Carlos E.","full_name":"Budde, Carlos E."},{"last_name":"Hartmanns","first_name":"Arnd","full_name":"Hartmanns, Arnd"},{"orcid":"0000-0002-1712-2165","full_name":"Meggendorfer, Tobias","first_name":"Tobias","last_name":"Meggendorfer","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1"},{"first_name":"Maximilian","last_name":"Weininger","id":"02ab0197-cc70-11ed-ab61-918e71f56881","full_name":"Weininger, Maximilian"},{"first_name":"Patrick","last_name":"Wienhöft","full_name":"Wienhöft, Patrick"}],"file_date_updated":"2025-06-02T09:35:42Z","date_created":"2025-05-25T22:17:08Z","language":[{"iso":"eng"}],"day":"01","publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","month":"05","date_published":"2025-05-01T00:00:00Z","ddc":["000"],"page":"167-190","status":"public","has_accepted_license":"1","department":[{"_id":"KrCh"}],"type":"conference","date_updated":"2025-06-02T09:45:41Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","doi":"10.1007/978-3-031-90643-5_9","volume":15696,"citation":{"chicago":"Budde, Carlos E., Arnd Hartmanns, Tobias Meggendorfer, Maximilian Weininger, and Patrick Wienhöft. “Sound Statistical Model Checking for Probabilities and Expected Rewards.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15696:167–90. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90643-5_9\">https://doi.org/10.1007/978-3-031-90643-5_9</a>.","mla":"Budde, Carlos E., et al. “Sound Statistical Model Checking for Probabilities and Expected Rewards.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15696, Springer Nature, 2025, pp. 167–90, doi:<a href=\"https://doi.org/10.1007/978-3-031-90643-5_9\">10.1007/978-3-031-90643-5_9</a>.","ama":"Budde CE, Hartmanns A, Meggendorfer T, Weininger M, Wienhöft P. Sound statistical model checking for probabilities and expected rewards. In: <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 15696. Springer Nature; 2025:167-190. doi:<a href=\"https://doi.org/10.1007/978-3-031-90643-5_9\">10.1007/978-3-031-90643-5_9</a>","apa":"Budde, C. E., Hartmanns, A., Meggendorfer, T., Weininger, M., &#38; Wienhöft, P. (2025). Sound statistical model checking for probabilities and expected rewards. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15696, pp. 167–190). Hamilton, ON, Canada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-90643-5_9\">https://doi.org/10.1007/978-3-031-90643-5_9</a>","ieee":"C. E. Budde, A. Hartmanns, T. Meggendorfer, M. Weininger, and P. Wienhöft, “Sound statistical model checking for probabilities and expected rewards,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Hamilton, ON, Canada, 2025, vol. 15696, pp. 167–190.","ista":"Budde CE, Hartmanns A, Meggendorfer T, Weininger M, Wienhöft P. 2025. Sound statistical model checking for probabilities and expected rewards. 31st 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. 15696, 167–190.","short":"C.E. Budde, A. Hartmanns, T. Meggendorfer, M. Weininger, P. Wienhöft, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 167–190."},"quality_controlled":"1","article_processing_charge":"No","file":[{"relation":"main_file","date_created":"2025-06-02T09:35:42Z","access_level":"open_access","success":1,"file_name":"2025_TACAS_Budde.pdf","checksum":"d45856b503b1dd4f8f14c3566327225b","creator":"dernst","date_updated":"2025-06-02T09:35:42Z","file_id":"19770","file_size":711271,"content_type":"application/pdf"}],"scopus_import":"1","OA_type":"hybrid","abstract":[{"text":"Statistical model checking estimates probabilities and expectations of interest in probabilistic system models by using random simulations. Its results come with statistical guarantees. However, many tools use unsound statistical methods that produce incorrect results more often than they claim. In this paper, we provide a comprehensive overview of tools and their correctness, as well as of sound methods available for estimating probabilities from the literature. For expected rewards, we investigate how to bound the path reward distribution to apply sound statistical methods for bounded distributions, of which we recommend the Dvoretzky-Kiefer-Wolfowitz inequality that has not been used in SMC so far. We prove that even reachability rewards can be bounded in theory, and formalise the concept of limit-PAC procedures for a practical solution. The modes SMC tool implements our methods and recommendations, which we use to experimentally confirm our results.","lang":"eng"}],"year":"2025","arxiv":1,"conference":{"location":"Hamilton, ON, Canada","end_date":"2025-05-08","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","start_date":"2025-05-03"},"oa":1,"ec_funded":1,"intvolume":"     15696","oa_version":"Published Version","title":"Sound statistical model checking for probabilities and expected rewards","publication_status":"published","_id":"19742","publisher":"Springer Nature","alternative_title":["LNCS"],"external_id":{"arxiv":["2411.00559"]},"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031906428"]},"project":[{"grant_number":"101034413","call_identifier":"H2020","name":"IST-BRIDGE: International postdoctoral program","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"}},{"corr_author":"1","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093.","OA_place":"publisher","related_material":{"record":[{"status":"public","id":"20147","relation":"dissertation_contains"}]},"language":[{"iso":"eng"}],"date_created":"2025-05-25T22:17:07Z","day":"01","file_date_updated":"2025-06-02T08:13:11Z","author":[{"id":"87e34708-d6c6-11ec-9f5b-9391e7be2463","last_name":"Chalupa","first_name":"Marek","full_name":"Chalupa, Marek"},{"full_name":"Henzinger, Thomas A","orcid":"0000-0002-2985-7724","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"},{"full_name":"Mazzocchi, Nicolas Adrien","id":"b26baa86-3308-11ec-87b0-8990f34baa85","last_name":"Mazzocchi","first_name":"Nicolas Adrien"},{"first_name":"Naci E","last_name":"Sarac","id":"8C6B42F8-C8E6-11E9-A03A-F2DCE5697425","full_name":"Sarac, Naci E"}],"status":"public","page":"303-312","month":"05","ddc":["000"],"date_published":"2025-05-01T00:00:00Z","publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","date_updated":"2026-07-27T12:48:18Z","type":"conference","has_accepted_license":"1","department":[{"_id":"ToHe"}],"doi":"10.1007/978-3-031-90643-5_16","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","citation":{"ista":"Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. 2025. Automating the analysis of quantitative automata with QuAK. 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems. , LNCS, vol. 15696, 303–312.","short":"M. Chalupa, T.A. Henzinger, N.A. Mazzocchi, N.E. Sarac, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 303–312.","ieee":"M. Chalupa, T. A. Henzinger, N. A. Mazzocchi, and N. E. Sarac, “Automating the analysis of quantitative automata with QuAK,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 2025, vol. 15696, pp. 303–312.","mla":"Chalupa, Marek, et al. “Automating the Analysis of Quantitative Automata with QuAK.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15696, Springer Nature, 2025, pp. 303–12, doi:<a href=\"https://doi.org/10.1007/978-3-031-90643-5_16\">10.1007/978-3-031-90643-5_16</a>.","ama":"Chalupa M, Henzinger TA, Mazzocchi NA, Sarac NE. Automating the analysis of quantitative automata with QuAK. In: <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 15696. Springer Nature; 2025:303-312. doi:<a href=\"https://doi.org/10.1007/978-3-031-90643-5_16\">10.1007/978-3-031-90643-5_16</a>","apa":"Chalupa, M., Henzinger, T. A., Mazzocchi, N. A., &#38; Sarac, N. E. (2025). Automating the analysis of quantitative automata with QuAK. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15696, pp. 303–312). Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-90643-5_16\">https://doi.org/10.1007/978-3-031-90643-5_16</a>","chicago":"Chalupa, Marek, Thomas A Henzinger, Nicolas Adrien Mazzocchi, and Naci E Sarac. “Automating the Analysis of Quantitative Automata with QuAK.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15696:303–12. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90643-5_16\">https://doi.org/10.1007/978-3-031-90643-5_16</a>."},"volume":15696,"file":[{"success":1,"file_name":"2025_TACAS_ChalupaMarek.pdf","relation":"main_file","access_level":"open_access","date_created":"2025-06-02T08:13:11Z","file_size":420669,"content_type":"application/pdf","file_id":"19768","date_updated":"2025-06-02T08:13:11Z","checksum":"a27fa245be8d83421e9127b48a09c8af","creator":"dernst"}],"article_processing_charge":"No","scopus_import":"1","year":"2025","abstract":[{"lang":"eng","text":"Quantitative automata model beyond-boolean aspects of systems: every execution is mapped to a real number by incorporating weighted transitions and value functions that generalize acceptance conditions of boolean w-automata. Despite the theoretical advances in systems analysis through quantitative automata, the first comprehensive software tool for quantitative automata (Quantitative Automata Kit, or QuAK) was developed only recently. QuAK implements algorithms for solving standard decision problems, e.g., emptiness and universality, as well as constructions for safety and liveness of quantitative automata. We present the architecture of QuAK, which reflects that all of these problems reduce to either checking inclusion between two quantitative automata or computing the highest value achievable by an automaton—its so-called top value. We improve QuAK by extending these two algorithms with an option to return, alongside their results, an ultimately periodic word witnessing the algorithm’s output, as well as implementing a new safety-liveness decomposition algorithm that can handle nondeterministic automata, making QuAK more informative and capable."}],"OA_type":"hybrid","arxiv":1,"intvolume":"     15696","ec_funded":1,"oa":1,"publication_status":"published","_id":"19741","title":"Automating the analysis of quantitative automata with QuAK","oa_version":"Published Version","publisher":"Springer Nature","publication_identifier":{"isbn":["9783031906428"],"issn":["0302-9743"],"eissn":["1611-3349"]},"external_id":{"arxiv":["2501.16088"]},"alternative_title":["LNCS"],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","image":"/images/cc_by.png","short":"CC BY (4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode"},"project":[{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093","call_identifier":"H2020"}]}]