[{"scopus_import":"1","citation":{"ieee":"K. Chatterjee, M. Jafariraviz, R. J. Saona Urmeneta, and J. Svoboda, “Value iteration with guessing for Markov chains and Markov decision processes,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Hamilton, ON, Canada, 2025, vol. 15697, pp. 217–236.","mla":"Chatterjee, Krishnendu, et al. “Value Iteration with Guessing for Markov Chains and Markov Decision Processes.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15697, Springer Nature, 2025, pp. 217–36, doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_11\">10.1007/978-3-031-90653-4_11</a>.","short":"K. Chatterjee, M. Jafariraviz, R.J. Saona Urmeneta, J. Svoboda, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 217–236.","chicago":"Chatterjee, Krishnendu, Mahdi Jafariraviz, Raimundo J Saona Urmeneta, and Jakub Svoboda. “Value Iteration with Guessing for Markov Chains and Markov Decision Processes.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15697:217–36. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_11\">https://doi.org/10.1007/978-3-031-90653-4_11</a>.","ama":"Chatterjee K, Jafariraviz M, Saona Urmeneta RJ, Svoboda J. Value iteration with guessing for Markov chains and Markov decision processes. In: <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 15697. Springer Nature; 2025:217-236. doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_11\">10.1007/978-3-031-90653-4_11</a>","ista":"Chatterjee K, Jafariraviz M, Saona Urmeneta RJ, Svoboda J. 2025. Value iteration with guessing for Markov chains and Markov decision processes. 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. 15697, 217–236.","apa":"Chatterjee, K., Jafariraviz, M., Saona Urmeneta, R. J., &#38; Svoboda, J. (2025). Value iteration with guessing for Markov chains and Markov decision processes. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15697, pp. 217–236). Hamilton, ON, Canada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_11\">https://doi.org/10.1007/978-3-031-90653-4_11</a>"},"month":"05","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","type":"conference","date_created":"2025-05-25T22:17:06Z","doi":"10.1007/978-3-031-90653-4_11","publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783031906527"]},"_id":"19740","acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt) grant and Austrian Science Fund (FWF) 10.55776/COE12 grant.","department":[{"_id":"KrCh"}],"oa":1,"oa_version":"Published Version","quality_controlled":"1","language":[{"iso":"eng"}],"OA_place":"publisher","title":"Value iteration with guessing for Markov chains and Markov decision processes","file_date_updated":"2025-06-02T07:31:12Z","abstract":[{"text":"Two standard models for probabilistic systems are Markov chains (MCs) and Markov decision processes (MDPs). Classic objectives for such probabilistic models for control and planning problems are reachability and stochastic shortest path. The widely studied algorithmic approach for these problems is the Value Iteration (VI) algorithm which iteratively applies local updates called Bellman updates. There are many practical approaches for VI in the literature but they all require exponentially many Bellman updates for MCs in the worst case. A preprocessing step is an algorithm that is discrete, graph-theoretical, and requires linear space. An important open question is whether, after a polynomial-time preprocessing, VI can be achieved with sub-exponentially many Bellman updates. In this work, we present a new approach for VI based on guessing values. Our theoretical contributions are twofold. First, for MCs, we present an almost-linear-time preprocessing algorithm after which, along with guessing values, VI requires only subexponentially many Bellman updates. Second, we present an improved analysis of the speed of convergence of VI for MDPs. Finally, we present a practical algorithm for MDPs based on our new approach. Experimental results show that our approach provides a considerable improvement over existing VI-based approaches on several benchmark examples from the literature.","lang":"eng"}],"publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","volume":15697,"alternative_title":["LNCS"],"ec_funded":1,"project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"external_id":{"arxiv":["2505.06769"]},"page":"217-236","conference":{"location":"Hamilton, ON, Canada","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","end_date":"2025-05-08","start_date":"2025-05-03"},"article_processing_charge":"No","arxiv":1,"publisher":"Springer Nature","date_updated":"2025-06-02T07:35:06Z","status":"public","publication_status":"published","license":"https://creativecommons.org/licenses/by/4.0/","file":[{"file_id":"19767","file_name":"2025_TACAS_Chatterjee.pdf","success":1,"access_level":"open_access","relation":"main_file","date_created":"2025-06-02T07:31:12Z","checksum":"45da6efbcbed20aada16c48c8e55e2d6","date_updated":"2025-06-02T07:31:12Z","content_type":"application/pdf","file_size":557481,"creator":"dernst"}],"day":"01","year":"2025","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee"},{"full_name":"Jafariraviz, Mahdi","first_name":"Mahdi","last_name":"Jafariraviz"},{"orcid":"0000-0001-5103-038X","full_name":"Saona Urmeneta, Raimundo J","id":"BD1DF4C4-D767-11E9-B658-BC13E6697425","first_name":"Raimundo J","last_name":"Saona Urmeneta"},{"id":"130759D2-D7DD-11E9-87D2-DE0DE6697425","full_name":"Svoboda, Jakub","orcid":"0000-0002-1419-3267","last_name":"Svoboda","first_name":"Jakub"}],"date_published":"2025-05-01T00:00:00Z","ddc":["000"],"OA_type":"hybrid","corr_author":"1","has_accepted_license":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"intvolume":"     15697"},{"file_date_updated":"2025-06-02T10:49:52Z","volume":15697,"ec_funded":1,"alternative_title":["LNCS"],"abstract":[{"lang":"eng","text":"The possibility of errors in human-engineered formal verification software, such as model checkers, poses a serious threat to the purpose of these tools. An established approach to mitigate this problem are certificates—lightweight, easy-to-check proofs of the verification results. In this paper, we develop novel certificates for model checking of Markov decision processes (MDPs) with quantitative reachability and expected reward properties. Our approach is conceptually simple and relies almost exclusively on elementary fixed point theory. Our certificates work for arbitrary finite MDPs and can be readily computed with little overhead using standard algorithms. We formalize the soundness of our certificates in Isabelle/HOL and provide a formally verified certificate checker. Moreover, we augment existing algorithms in the probabilistic model checker Storm with the ability to produce certificates and demonstrate practical applicability by conducting the first formal certification of the reference results in the Quantitative Verification Benchmark Set."}],"publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","title":"Fixed point certificates for reachability and expected rewards in MDPs","arxiv":1,"project":[{"grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"},{"name":"IST-BRIDGE: International postdoctoral program","call_identifier":"H2020","_id":"fc2ed2f7-9c52-11eb-aca3-c01059dda49c","grant_number":"101034413"}],"article_processing_charge":"No","external_id":{"arxiv":["2501.11467"]},"page":"130-151","conference":{"name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","location":"Hamilton, ON, Canada","end_date":"2025-05-08","start_date":"2025-05-03"},"_id":"19743","related_material":{"record":[{"id":"19771","status":"public","relation":"research_data"}]},"publication_identifier":{"isbn":["9783031906527"],"issn":["0302-9743"],"eissn":["1611-3349"]},"doi":"10.1007/978-3-031-90653-4_7","date_created":"2025-05-25T22:17:09Z","acknowledgement":"This project has received funding from the ERC CoG 863818 (ForM-SMArt), the Austrian Science Fund (FWF) 10.55776/COE12, a KI-Starter grant from the Ministerium für Kultur und Wissenschaft NRW, the DFG RTG 378803395 (ConVeY), the EU’s Horizon 2020 research and innovation programmes under the Marie Sklodowska-Curie grant agreement Nos. 101034413 (IST-BRIDGE) and 101008233 (MISSION), and the DFG RTG 2236 (UnRAVeL). Experiments were performed with computing resources granted by RWTH Aachen University under project rwth1632.","citation":{"apa":"Chatterjee, K., Quatmann, T., Schäffeler, M., Weininger, M., Winkler, T., &#38; Zilken, D. (2025). Fixed point certificates for reachability and expected rewards in MDPs. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15697, pp. 130–151). Hamilton, ON, Canada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_7\">https://doi.org/10.1007/978-3-031-90653-4_7</a>","ista":"Chatterjee K, Quatmann T, Schäffeler M, Weininger M, Winkler T, Zilken D. 2025. Fixed point certificates for reachability and expected rewards in MDPs. 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. 15697, 130–151.","chicago":"Chatterjee, Krishnendu, Tim Quatmann, Maximilian Schäffeler, Maximilian Weininger, Tobias Winkler, and Daniel Zilken. “Fixed Point Certificates for Reachability and Expected Rewards in MDPs.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15697:130–51. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_7\">https://doi.org/10.1007/978-3-031-90653-4_7</a>.","ama":"Chatterjee K, Quatmann T, Schäffeler M, Weininger M, Winkler T, Zilken D. Fixed point certificates for reachability and expected rewards in MDPs. In: <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 15697. Springer Nature; 2025:130-151. doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_7\">10.1007/978-3-031-90653-4_7</a>","ieee":"K. Chatterjee, T. Quatmann, M. Schäffeler, M. Weininger, T. Winkler, and D. Zilken, “Fixed point certificates for reachability and expected rewards in MDPs,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Hamilton, ON, Canada, 2025, vol. 15697, pp. 130–151.","mla":"Chatterjee, Krishnendu, et al. “Fixed Point Certificates for Reachability and Expected Rewards in MDPs.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15697, Springer Nature, 2025, pp. 130–51, doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_7\">10.1007/978-3-031-90653-4_7</a>.","short":"K. Chatterjee, T. Quatmann, M. Schäffeler, M. Weininger, T. Winkler, D. Zilken, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 130–151."},"scopus_import":"1","type":"conference","month":"05","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","language":[{"iso":"eng"}],"OA_place":"publisher","department":[{"_id":"KrCh"}],"oa_version":"Published Version","oa":1,"date_published":"2025-05-01T00:00:00Z","ddc":["000"],"OA_type":"hybrid","corr_author":"1","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Tim","last_name":"Quatmann","full_name":"Quatmann, Tim"},{"full_name":"Schäffeler, Maximilian","first_name":"Maximilian","last_name":"Schäffeler"},{"full_name":"Weininger, Maximilian","id":"02ab0197-cc70-11ed-ab61-918e71f56881","first_name":"Maximilian","last_name":"Weininger"},{"first_name":"Tobias","last_name":"Winkler","full_name":"Winkler, Tobias"},{"first_name":"Daniel","last_name":"Zilken","full_name":"Zilken, Daniel","id":"d8ebc24a-3f98-11f0-9044-8296d4f39ab3"}],"tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"intvolume":"     15697","has_accepted_license":"1","publication_status":"published","status":"public","publisher":"Springer Nature","date_updated":"2025-06-02T10:55:34Z","day":"01","year":"2025","file":[{"date_created":"2025-06-02T10:49:52Z","checksum":"64b7f46ef05649b87b827248045c7645","relation":"main_file","access_level":"open_access","creator":"dernst","content_type":"application/pdf","date_updated":"2025-06-02T10:49:52Z","file_size":732136,"file_name":"2025_TACAS_ChatterjeeKrish.pdf","file_id":"19772","success":1}]},{"department":[{"_id":"KrCh"}],"oa":1,"oa_version":"Published Version","quality_controlled":"1","language":[{"iso":"eng"}],"OA_place":"publisher","citation":{"ista":"Chatterjee K, Goharshady E, Novotný P, Zikelic D. 2025. Refuting equivalence in probabilistic programs with conditioning. 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. 15697, 279–300.","apa":"Chatterjee, K., Goharshady, E., Novotný, P., &#38; Zikelic, D. (2025). Refuting equivalence in probabilistic programs with conditioning. In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i> (Vol. 15697, pp. 279–300). Hamilton, ON, Canada: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_14\">https://doi.org/10.1007/978-3-031-90653-4_14</a>","short":"K. Chatterjee, E. Goharshady, P. Novotný, D. Zikelic, in:, 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer Nature, 2025, pp. 279–300.","mla":"Chatterjee, Krishnendu, et al. “Refuting Equivalence in Probabilistic Programs with Conditioning.” <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, vol. 15697, Springer Nature, 2025, pp. 279–300, doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_14\">10.1007/978-3-031-90653-4_14</a>.","ieee":"K. Chatterjee, E. Goharshady, P. Novotný, and D. Zikelic, “Refuting equivalence in probabilistic programs with conditioning,” in <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, Hamilton, ON, Canada, 2025, vol. 15697, pp. 279–300.","ama":"Chatterjee K, Goharshady E, Novotný P, Zikelic D. Refuting equivalence in probabilistic programs with conditioning. In: <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>. Vol 15697. Springer Nature; 2025:279-300. doi:<a href=\"https://doi.org/10.1007/978-3-031-90653-4_14\">10.1007/978-3-031-90653-4_14</a>","chicago":"Chatterjee, Krishnendu, Ehsan Goharshady, Petr Novotný, and Dorde Zikelic. “Refuting Equivalence in Probabilistic Programs with Conditioning.” In <i>31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems</i>, 15697:279–300. Springer Nature, 2025. <a href=\"https://doi.org/10.1007/978-3-031-90653-4_14\">https://doi.org/10.1007/978-3-031-90653-4_14</a>."},"scopus_import":"1","type":"conference","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","month":"05","publication_identifier":{"isbn":["9783031906527"],"issn":["0302-9743"],"eissn":["1611-3349"]},"_id":"19744","doi":"10.1007/978-3-031-90653-4_14","date_created":"2025-05-25T22:17:10Z","acknowledgement":"This work was partially supported by ERC CoG 863818 (ForM-SMArt) and Austrian Science Fund (FWF) 10.55776/COE12. Petr Novotný is supported by the Czech Science Foundation grant no. GA23-06963S.","project":[{"grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"}],"article_processing_charge":"No","page":"279-300","external_id":{"arxiv":["2501.06579"]},"conference":{"end_date":"2025-05-08","start_date":"2025-05-03","location":"Hamilton, ON, Canada","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"arxiv":1,"title":"Refuting equivalence in probabilistic programs with conditioning","file_date_updated":"2025-06-02T11:13:49Z","ec_funded":1,"alternative_title":["LNCS"],"volume":15697,"abstract":[{"lang":"eng","text":"We consider the problem of refuting equivalence of probabilistic programs, i.e., the problem of proving that two probabilistic programs induce different output distributions. We study this problem in the context of programs with conditioning (i.e., with observe and score statements), where the output distribution is conditioned by the event that all the observe statements along a run evaluate to true, and where the probability densities of different runs may be updated via the score statements. Building on a recent work on programs without conditioning, we present a new equivalence refutation method for programs with conditioning. Our method is based on weighted restarting, a novel transformation of probabilistic programs with conditioning to the output equivalent probabilistic programs without conditioning that we introduce in this work. Our method is the first to be both a) fully automated, and b) providing provably correct answers. We demonstrate the applicability of our method on a set of programs from the probabilistic inference literature."}],"publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","file":[{"creator":"dernst","date_updated":"2025-06-02T11:13:49Z","content_type":"application/pdf","file_size":532181,"date_created":"2025-06-02T11:13:49Z","checksum":"7dcd85e7e753bfa994c10b3cf9ebc185","relation":"main_file","access_level":"open_access","success":1,"file_name":"2025_TACAS_Chatterjee_Goharshadi.pdf","file_id":"19773"}],"day":"01","year":"2025","publisher":"Springer Nature","date_updated":"2025-06-02T11:16:13Z","publication_status":"published","status":"public","has_accepted_license":"1","tmp":{"name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png"},"intvolume":"     15697","author":[{"orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu"},{"first_name":"Ehsan","last_name":"Kafshdar Goharshadi","orcid":"0000-0002-8595-0587","full_name":"Kafshdar Goharshadi, Ehsan","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d"},{"full_name":"Novotný, Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","first_name":"Petr","last_name":"Novotný"},{"full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","first_name":"Dorde","last_name":"Zikelic"}],"ddc":["000"],"date_published":"2025-05-01T00:00:00Z","corr_author":"1","OA_type":"hybrid"}]