[{"month":"03","scopus_import":"1","_id":"21661","tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"OA_place":"publisher","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication_status":"epub_ahead","citation":{"short":"A. Hartmanns, S. Junges, T. Quatmann, M. Weininger, International Journal on Software Tools for Technology Transfer (2026).","ista":"Hartmanns A, Junges S, Quatmann T, Weininger M. 2026. The revised practitioner’s guide to MDP model checking algorithms. International Journal on Software Tools for Technology Transfer.","mla":"Hartmanns, Arnd, et al. “The Revised Practitioner’s Guide to MDP Model Checking Algorithms.” <i>International Journal on Software Tools for Technology Transfer</i>, Springer Nature, 2026, doi:<a href=\"https://doi.org/10.1007/s10009-026-00848-y\">10.1007/s10009-026-00848-y</a>.","chicago":"Hartmanns, Arnd, Sebastian Junges, Tim Quatmann, and Maximilian Weininger. “The Revised Practitioner’s Guide to MDP Model Checking Algorithms.” <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature, 2026. <a href=\"https://doi.org/10.1007/s10009-026-00848-y\">https://doi.org/10.1007/s10009-026-00848-y</a>.","apa":"Hartmanns, A., Junges, S., Quatmann, T., &#38; Weininger, M. (2026). The revised practitioner’s guide to MDP model checking algorithms. <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s10009-026-00848-y\">https://doi.org/10.1007/s10009-026-00848-y</a>","ama":"Hartmanns A, Junges S, Quatmann T, Weininger M. The revised practitioner’s guide to MDP model checking algorithms. <i>International Journal on Software Tools for Technology Transfer</i>. 2026. doi:<a href=\"https://doi.org/10.1007/s10009-026-00848-y\">10.1007/s10009-026-00848-y</a>","ieee":"A. Hartmanns, S. Junges, T. Quatmann, and M. Weininger, “The revised practitioner’s guide to MDP model checking algorithms,” <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature, 2026."},"type":"journal_article","oa":1,"date_published":"2026-03-09T00:00:00Z","language":[{"iso":"eng"}],"doi":"10.1007/s10009-026-00848-y","publisher":"Springer Nature","article_type":"original","keyword":["Quantitative model checking","Markov decision process","Linear programming","Value iteration","Policy iteration"],"quality_controlled":"1","year":"2026","title":"The revised practitioner’s guide to MDP model checking algorithms","ddc":["000"],"day":"09","has_accepted_license":"1","OA_type":"hybrid","department":[{"_id":"KrCh"}],"project":[{"name":"IST-BRIDGE: International postdoctoral program","call_identifier":"H2020","grant_number":"101034413","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c"}],"author":[{"first_name":"Arnd","last_name":"Hartmanns","full_name":"Hartmanns, Arnd"},{"first_name":"Sebastian","full_name":"Junges, Sebastian","last_name":"Junges"},{"first_name":"Tim","full_name":"Quatmann, Tim","last_name":"Quatmann"},{"full_name":"Weininger, Maximilian","last_name":"Weininger","orcid":"0000-0002-0163-2152","first_name":"Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881"}],"oa_version":"Published Version","date_updated":"2026-04-07T09:52:54Z","abstract":[{"lang":"eng","text":"Model checking undiscounted reachability and expected-reward properties on Markov decision processes (MDPs) are key for the verification of systems that act under uncertainty. Popular algorithms are policy iteration and variants of value iteration; in tool competitions, most participants rely on the latter. These algorithms generally need worst-case exponential time. However, the problem can equally be formulated as a linear programme, solvable in polynomial time. In this paper, we give a detailed overview of today’s state-of-the-art algorithms for MDP model checking with a focus on performance and correctness. We highlight their fundamental differences, and describe various optimizations and implementation variants. We experimentally compare floating-point and exact-arithmetic implementations of all algorithms on three benchmark sets using two probabilistic model checkers. Our results show that (optimistic) value iteration is a sensible default, but other algorithms are preferable in specific settings. This paper thereby provides a guide for MDP verification practitioners—tool builders and users alike."}],"date_created":"2026-04-05T22:01:32Z","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1007/s10009-026-00848-y"}],"status":"public","acknowledgement":"This research was funded by the European Union’s Horizon 2020 research and innovation programme under Marie Skłodowska-Curie grant agreements 101008233 (MISSION)\r\nand 101034413 (IST-BRIDGE), by the Interreg North Sea project STORM_SAFE, by a KI-Starter grant from the Ministerium für Kultur und Wissenschaft NRW, by NWO VENI grant no. 639.021.754, and by NWO VIDI grant VI.Vidi.223.110 (TruSTy). Experiments were performed with computing resources granted by RWTH Aachen University under project rwth1632.","article_processing_charge":"Yes (in subscription journal)","ec_funded":1,"publication_identifier":{"eissn":["1433-2787"],"issn":["1433-2779"]},"publication":"International Journal on Software Tools for Technology Transfer","related_material":{"record":[{"id":"21668","relation":"software","status":"public"}]}},{"page":"575-592","external_id":{"arxiv":["2009.06429"],"isi":["001020160000001"]},"quality_controlled":"1","year":"2023","language":[{"iso":"eng"}],"doi":"10.1007/s10009-023-00711-4","publisher":"Springer Nature","date_published":"2023-08-01T00:00:00Z","file":[{"file_id":"14903","checksum":"3c4b347f39412a76872f9a6f30101f94","access_level":"open_access","file_name":"2023_JourSoftwareTools_Kueffner.pdf","date_updated":"2024-01-30T12:06:07Z","content_type":"application/pdf","file_size":13387667,"date_created":"2024-01-30T12:06:07Z","creator":"dernst","relation":"main_file","success":1}],"oa":1,"article_type":"original","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","corr_author":"1","volume":25,"type":"journal_article","publication_status":"published","citation":{"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.","mla":"Kueffner, Konstantin, et al. “Into the Unknown: Active Monitoring of Neural Networks (Extended Version).” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 25, Springer Nature, 2023, pp. 575–92, doi:<a href=\"https://doi.org/10.1007/s10009-023-00711-4\">10.1007/s10009-023-00711-4</a>.","chicago":"Kueffner, Konstantin, Anna Lukina, Christian Schilling, and Thomas A Henzinger. “Into the Unknown: Active Monitoring of Neural Networks (Extended Version).” <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature, 2023. <a href=\"https://doi.org/10.1007/s10009-023-00711-4\">https://doi.org/10.1007/s10009-023-00711-4</a>.","short":"K. Kueffner, A. Lukina, C. Schilling, T.A. Henzinger, International Journal on Software Tools for Technology Transfer 25 (2023) 575–592.","apa":"Kueffner, K., Lukina, A., Schilling, C., &#38; Henzinger, T. A. (2023). Into the unknown: Active monitoring of neural networks (extended version). <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s10009-023-00711-4\">https://doi.org/10.1007/s10009-023-00711-4</a>","ama":"Kueffner K, Lukina A, Schilling C, Henzinger TA. Into the unknown: Active monitoring of neural networks (extended version). <i>International Journal on Software Tools for Technology Transfer</i>. 2023;25:575-592. doi:<a href=\"https://doi.org/10.1007/s10009-023-00711-4\">10.1007/s10009-023-00711-4</a>","ieee":"K. Kueffner, A. Lukina, C. Schilling, and T. A. Henzinger, “Into the unknown: Active monitoring of neural networks (extended version),” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 25. Springer Nature, pp. 575–592, 2023."},"scopus_import":"1","month":"08","arxiv":1,"_id":"13234","tmp":{"short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png"},"publication_identifier":{"eissn":["1433-2787"],"issn":["1433-2779"]},"ec_funded":1,"publication":"International Journal on Software Tools for Technology Transfer","related_material":{"record":[{"status":"public","id":"10206","relation":"shorter_version"}]},"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.","date_created":"2023-07-16T22:01:11Z","file_date_updated":"2024-01-30T12:06:07Z","status":"public","article_processing_charge":"Yes (in subscription journal)","author":[{"full_name":"Kueffner, Konstantin","last_name":"Kueffner","orcid":"0000-0001-8974-2542","first_name":"Konstantin","id":"8121a2d0-dc85-11ea-9058-af578f3b4515"},{"last_name":"Lukina","full_name":"Lukina, Anna","first_name":"Anna","id":"CBA4D1A8-0FE8-11E9-BDE6-07BFE5697425"},{"orcid":"0000-0003-3658-1065","first_name":"Christian","id":"3A2F4DCE-F248-11E8-B48F-1D18A9856A87","full_name":"Schilling, Christian","last_name":"Schilling"},{"full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas A"}],"abstract":[{"lang":"eng","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."}],"oa_version":"Published Version","intvolume":"        25","date_updated":"2025-04-15T06:55:00Z","ddc":["000"],"day":"01","title":"Into the unknown: Active monitoring of neural networks (extended version)","department":[{"_id":"ToHe"}],"project":[{"name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","grant_number":"101020093","call_identifier":"H2020"}],"isi":1,"has_accepted_license":"1"},{"title":"AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic","day":"03","isi":1,"department":[{"_id":"ToHe"}],"author":[{"last_name":"Nickovic","full_name":"Nickovic, Dejan","first_name":"Dejan","id":"41BCEE5C-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Lebeltel, Olivier","last_name":"Lebeltel","first_name":"Olivier"},{"first_name":"Oded","last_name":"Maler","full_name":"Maler, Oded"},{"last_name":"Ferrere","full_name":"Ferrere, Thomas","id":"40960E6E-F248-11E8-B48F-1D18A9856A87","first_name":"Thomas","orcid":"0000-0001-5199-3143"},{"last_name":"Ulus","full_name":"Ulus, Dogan","first_name":"Dogan"}],"date_updated":"2024-10-09T20:58:18Z","intvolume":"        22","oa_version":"None","abstract":[{"lang":"eng","text":"We introduce in this paper AMT2.0, a tool for qualitative and quantitative analysis of hybrid continuous and Boolean signals that combine numerical values and discrete events. The evaluation of the signals is based on rich temporal specifications expressed in extended signal temporal logic, which integrates timed regular expressions within signal temporal logic. The tool features qualitative monitoring (property satisfaction checking), trace diagnostics for explaining and justifying property violations and specification-driven measurement of quantitative features of the signal. We demonstrate the tool functionality on several running examples and case studies, and evaluate its performance."}],"status":"public","date_created":"2022-03-18T10:10:53Z","article_processing_charge":"No","publication_identifier":{"issn":["1433-2779"],"eissn":["1433-2787"]},"publication":"International Journal on Software Tools for Technology Transfer","related_material":{"record":[{"relation":"earlier_version","id":"299","status":"public"}]},"scopus_import":"1","month":"08","_id":"10861","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"short":"D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, D. Ulus, International Journal on Software Tools for Technology Transfer 22 (2020) 741–758.","chicago":"Nickovic, Dejan, Olivier Lebeltel, Oded Maler, Thomas Ferrere, and Dogan Ulus. “AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic.” <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature, 2020. <a href=\"https://doi.org/10.1007/s10009-020-00582-z\">https://doi.org/10.1007/s10009-020-00582-z</a>.","ista":"Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. 2020. AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. International Journal on Software Tools for Technology Transfer. 22(6), 741–758.","mla":"Nickovic, Dejan, et al. “AMT 2.0: Qualitative and Quantitative Trace Analysis with Extended Signal Temporal Logic.” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 22, no. 6, Springer Nature, 2020, pp. 741–58, doi:<a href=\"https://doi.org/10.1007/s10009-020-00582-z\">10.1007/s10009-020-00582-z</a>.","apa":"Nickovic, D., Lebeltel, O., Maler, O., Ferrere, T., &#38; Ulus, D. (2020). AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. <i>International Journal on Software Tools for Technology Transfer</i>. Springer Nature. <a href=\"https://doi.org/10.1007/s10009-020-00582-z\">https://doi.org/10.1007/s10009-020-00582-z</a>","ama":"Nickovic D, Lebeltel O, Maler O, Ferrere T, Ulus D. AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic. <i>International Journal on Software Tools for Technology Transfer</i>. 2020;22(6):741-758. doi:<a href=\"https://doi.org/10.1007/s10009-020-00582-z\">10.1007/s10009-020-00582-z</a>","ieee":"D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, and D. Ulus, “AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic,” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 22, no. 6. Springer Nature, pp. 741–758, 2020."},"publication_status":"published","volume":22,"type":"journal_article","issue":"6","language":[{"iso":"eng"}],"publisher":"Springer Nature","date_published":"2020-08-03T00:00:00Z","doi":"10.1007/s10009-020-00582-z","article_type":"original","keyword":["Information Systems","Software"],"external_id":{"isi":["000555398600001"]},"page":"741-758","year":"2020","quality_controlled":"1"}]