[{"publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"isbn":["9783031906527"]},"ec_funded":1,"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.","publication":"31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems","scopus_import":"1","language":[{"iso":"eng"}],"OA_place":"publisher","OA_type":"hybrid","oa_version":"Published Version","type":"conference","abstract":[{"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.","lang":"eng"}],"_id":"19744","title":"Refuting equivalence in probabilistic programs with conditioning","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-8595-0587","full_name":"Kafshdar Goharshadi, Ehsan","last_name":"Kafshdar Goharshadi","first_name":"Ehsan","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d"},{"last_name":"Novotný","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotný, Petr"},{"full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","last_name":"Zikelic"}],"date_created":"2025-05-25T22:17:10Z","status":"public","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2026-09-16T06:57:43Z","project":[{"grant_number":"863818","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020"},{"_id":"4029cfc7-b034-11f1-9e55-88ab2ff3b6ee","name":"Bilateral Artificial Intelligence (Chatterjee)","grant_number":"COE12"}],"citation":{"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>","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.","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.","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.","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>.","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>"},"page":"279-300","external_id":{"arxiv":["2501.06579"]},"month":"05","department":[{"_id":"KrCh"}],"publisher":"Springer Nature","day":"01","oa":1,"corr_author":"1","volume":15697,"file":[{"file_id":"19773","content_type":"application/pdf","date_updated":"2025-06-02T11:13:49Z","file_name":"2025_TACAS_Chatterjee_Goharshadi.pdf","file_size":532181,"success":1,"checksum":"7dcd85e7e753bfa994c10b3cf9ebc185","date_created":"2025-06-02T11:13:49Z","access_level":"open_access","relation":"main_file","creator":"dernst"}],"doi":"10.1007/978-3-031-90653-4_14","year":"2025","quality_controlled":"1","publication_status":"published","intvolume":"     15697","ddc":["000"],"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"fulldoi":"https://doi.org/10.1007/978-3-031-90653-4_14","arxiv":1,"alternative_title":["LNCS"],"file_date_updated":"2025-06-02T11:13:49Z","date_published":"2025-05-01T00:00:00Z","has_accepted_license":"1","conference":{"location":"Hamilton, ON, Canada","start_date":"2025-05-03","end_date":"2025-05-08","name":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems"},"article_processing_charge":"No"},{"_id":"18160","title":"Solving long-run average reward robust MDPs via stochastic games","date_created":"2024-09-29T22:01:39Z","status":"public","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","first_name":"Ehsan","last_name":"Kafshdar Goharshadi","orcid":"0000-0002-8595-0587","full_name":"Kafshdar Goharshadi, Ehsan"},{"full_name":"Karrabi, Mehrdad","orcid":"0009-0007-5253-9170","first_name":"Mehrdad","last_name":"Karrabi","id":"67638922-f394-11eb-9cf6-f20423e08757"},{"last_name":"Novotný","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotný, Petr"},{"first_name":"Dorde","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde"}],"oa_version":"Preprint","type":"conference","abstract":[{"text":"Markov decision processes (MDPs) provide a standard framework for sequential decision making under uncertainty. However, MDPs do not take uncertainty in transition probabilities into account. Robust Markov decision processes (RMDPs) address this shortcoming of MDPs by assigning to each transition an uncertainty set rather than a single probability value. In this work, we consider polytopic RMDPs in which all uncertainty sets are polytopes and study the problem of solving long-run average reward polytopic RMDPs. We present a novel perspective on this problem and show that it can be reduced to solving long-run average reward turn-based stochastic games with finite state and action spaces. This reduction allows us to derive several important consequences that were hitherto not known to hold for polytopic RMDPs. First, we derive new computational complexity bounds for solving long-run average reward polytopic RMDPs, showing for the first time that the threshold decision problem for them is in NP∩CONP and that they admit a randomized algorithm with sub-exponential expected runtime. Second, we present Robust Polytopic Policy Iteration (RPPI), a novel policy iteration algorithm for solving long-run average reward polytopic RMDPs. Our experimental evaluation shows that RPPI is much more efficient in solving long-run average reward polytopic RMDPs compared to state-of-the-art methods based on value iteration. ","lang":"eng"}],"project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"}],"citation":{"apa":"Chatterjee, K., Goharshady, E., Karrabi, M., Novotný, P., &#38; Zikelic, D. (2024). Solving long-run average reward robust MDPs via stochastic games. In <i>33rd International Joint Conference on Artificial Intelligence</i> (pp. 6707–6715). Jeju, South Korea: International Joint Conferences on Artificial Intelligence. <a href=\"https://doi.org/10.24963/ijcai.2024/741\">https://doi.org/10.24963/ijcai.2024/741</a>","chicago":"Chatterjee, Krishnendu, Ehsan Goharshady, Mehrdad Karrabi, Petr Novotný, and Dorde Zikelic. “Solving Long-Run Average Reward Robust MDPs via Stochastic Games.” In <i>33rd International Joint Conference on Artificial Intelligence</i>, 6707–15. International Joint Conferences on Artificial Intelligence, 2024. <a href=\"https://doi.org/10.24963/ijcai.2024/741\">https://doi.org/10.24963/ijcai.2024/741</a>.","short":"K. Chatterjee, E. Goharshady, M. Karrabi, P. Novotný, D. Zikelic, in:, 33rd International Joint Conference on Artificial Intelligence, International Joint Conferences on Artificial Intelligence, 2024, pp. 6707–6715.","ieee":"K. Chatterjee, E. Goharshady, M. Karrabi, P. Novotný, and D. Zikelic, “Solving long-run average reward robust MDPs via stochastic games,” in <i>33rd International Joint Conference on Artificial Intelligence</i>, Jeju, South Korea, 2024, pp. 6707–6715.","ista":"Chatterjee K, Goharshady E, Karrabi M, Novotný P, Zikelic D. 2024. Solving long-run average reward robust MDPs via stochastic games. 33rd International Joint Conference on Artificial Intelligence. IJCAI: International Joint Conference on Artificial Intelligence, 6707–6715.","ama":"Chatterjee K, Goharshady E, Karrabi M, Novotný P, Zikelic D. Solving long-run average reward robust MDPs via stochastic games. In: <i>33rd International Joint Conference on Artificial Intelligence</i>. International Joint Conferences on Artificial Intelligence; 2024:6707-6715. doi:<a href=\"https://doi.org/10.24963/ijcai.2024/741\">10.24963/ijcai.2024/741</a>","mla":"Chatterjee, Krishnendu, et al. “Solving Long-Run Average Reward Robust MDPs via Stochastic Games.” <i>33rd International Joint Conference on Artificial Intelligence</i>, International Joint Conferences on Artificial Intelligence, 2024, pp. 6707–15, doi:<a href=\"https://doi.org/10.24963/ijcai.2024/741\">10.24963/ijcai.2024/741</a>."},"page":"6707-6715","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","supplementarymaterial":"no","date_updated":"2026-10-16T08:07:05Z","publication":"33rd International Joint Conference on Artificial Intelligence","scopus_import":"1","publication_identifier":{"issn":["1045-0823"],"isbn":["9781956792041"]},"ec_funded":1,"acknowledgement":"This work was supported in part by the ERC-2020-CoG 863818 (FoRM-SMArt) and the Czech Science Foundation\r\ngrant no. GA23-06963S.","OA_place":"repository","OA_type":"green","language":[{"iso":"eng"}],"year":"2024","quality_controlled":"1","publication_status":"published","date_published":"2024-09-01T00:00:00Z","conference":{"location":"Jeju, South Korea","name":"IJCAI: International Joint Conference on Artificial Intelligence","start_date":"2024-08-03","end_date":"2024-08-09"},"article_processing_charge":"No","fulldoi":"https://doi.org/10.24963/ijcai.2024/741","das_tickbox":"0","arxiv":1,"main_file_link":[{"url":"https://doi.org/10.48550/arXiv.2312.13912","open_access":"1"}],"day":"01","corr_author":"1","oa":1,"external_id":{"arxiv":["2312.13912"]},"month":"09","department":[{"_id":"KrCh"}],"publisher":"International Joint Conferences on Artificial Intelligence","researchdata_availability":"no","doi":"10.24963/ijcai.2024/741"},{"intvolume":"         8","publication_status":"published","year":"2024","quality_controlled":"1","tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"ddc":["000"],"arxiv":1,"das_tickbox":"0","fulldoi":"https://doi.org/10.1145/3656462","article_processing_charge":"Yes (via OA deal)","has_accepted_license":"1","file_date_updated":"2024-07-22T07:17:14Z","date_published":"2024-06-20T00:00:00Z","publisher":"Association for Computing Machinery","month":"06","department":[{"_id":"KrCh"},{"_id":"GradSch"}],"external_id":{"arxiv":["2404.03430"]},"oa":1,"corr_author":"1","day":"20","researchdata_availability":"no","doi":"10.1145/3656462","file":[{"file_id":"17290","date_updated":"2024-07-22T07:17:14Z","content_type":"application/pdf","file_name":"2024_ACMProgLang_Chatterjee.pdf","file_size":355421,"success":1,"checksum":"8cbf220f284a4a87d093db5320c5afdd","date_created":"2024-07-22T07:17:14Z","access_level":"open_access","relation":"main_file","creator":"dernst"}],"volume":8,"article_number":"232","abstract":[{"text":"We consider the problems of statically refuting equivalence and similarity of output distributions defined by a pair of probabilistic programs. Equivalence and similarity are two fundamental relational properties of probabilistic programs that are essential for their correctness both in implementation and in compilation. In this work, we present a new method for static equivalence and similarity refutation. Our method refutes equivalence and similarity by computing a function over program outputs whose expected value with respect to the output distributions of two programs is different. The function is computed simultaneously with an upper expectation supermartingale and a lower expectation submartingale for the two programs, which we show to together provide a formal certificate for refuting equivalence and similarity. To the best of our knowledge, our method is the first approach to relational program analysis to offer the combination of the following desirable features: (1) it is fully automated, (2) it is applicable to infinite-state probabilistic programs, and (3) it provides formal guarantees on the correctness of its results. We implement a prototype of our method and our experiments demonstrate the effectiveness of our method to refute equivalence and similarity for a number of examples collected from the literature.","lang":"eng"}],"type":"journal_article","oa_version":"Published Version","article_type":"original","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"first_name":"Ehsan","last_name":"Kafshdar Goharshadi","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","orcid":"0000-0002-8595-0587","full_name":"Kafshdar Goharshadi, Ehsan"},{"id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","last_name":"Novotný","first_name":"Petr","full_name":"Novotný, Petr"},{"first_name":"Dorde","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699"}],"date_created":"2024-07-21T22:01:01Z","status":"public","title":"Equivalence and similarity refutation for probabilistic programs","_id":"17283","date_updated":"2026-10-16T08:08:51Z","supplementarymaterial":"no","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","citation":{"mla":"Chatterjee, Krishnendu, et al. “Equivalence and Similarity Refutation for Probabilistic Programs.” <i>Proceedings of the ACM on Programming Languages</i>, vol. 8, 232, Association for Computing Machinery, 2024, doi:<a href=\"https://doi.org/10.1145/3656462\">10.1145/3656462</a>.","ama":"Chatterjee K, Goharshady E, Novotný P, Zikelic D. Equivalence and similarity refutation for probabilistic programs. <i>Proceedings of the ACM on Programming Languages</i>. 2024;8. doi:<a href=\"https://doi.org/10.1145/3656462\">10.1145/3656462</a>","ista":"Chatterjee K, Goharshady E, Novotný P, Zikelic D. 2024. Equivalence and similarity refutation for probabilistic programs. Proceedings of the ACM on Programming Languages. 8, 232.","ieee":"K. Chatterjee, E. Goharshady, P. Novotný, and D. Zikelic, “Equivalence and similarity refutation for probabilistic programs,” <i>Proceedings of the ACM on Programming Languages</i>, vol. 8. Association for Computing Machinery, 2024.","short":"K. Chatterjee, E. Goharshady, P. Novotný, D. Zikelic, Proceedings of the ACM on Programming Languages 8 (2024).","chicago":"Chatterjee, Krishnendu, Ehsan Goharshady, Petr Novotný, and Dorde Zikelic. “Equivalence and Similarity Refutation for Probabilistic Programs.” <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery, 2024. <a href=\"https://doi.org/10.1145/3656462\">https://doi.org/10.1145/3656462</a>.","apa":"Chatterjee, K., Goharshady, E., Novotný, P., &#38; Zikelic, D. (2024). Equivalence and similarity refutation for probabilistic programs. <i>Proceedings of the ACM on Programming Languages</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3656462\">https://doi.org/10.1145/3656462</a>"},"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"}],"ec_funded":1,"acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt) grant. Petr Novotný\r\nis supported by the Czech Science Foundation grant no. GA23-06963S.\r\n","publication_identifier":{"eissn":["2475-1421"]},"scopus_import":"1","publication":"Proceedings of the ACM on Programming Languages","language":[{"iso":"eng"}],"OA_type":"hybrid","OA_place":"publisher"},{"volume":35,"file":[{"content_type":"application/pdf","date_updated":"2024-01-16T08:11:24Z","file_name":"2023_FormalAspectsComputing_Chatterjee.pdf","file_size":502522,"file_id":"14804","access_level":"open_access","creator":"dernst","relation":"main_file","success":1,"checksum":"3bb133eeb27ec01649a9a36445d952d9","date_created":"2024-01-16T08:11:24Z"}],"doi":"10.1145/3585391","article_number":"11","isi":1,"external_id":{"arxiv":["2108.02188"],"isi":["001035915800006"]},"department":[{"_id":"KrCh"}],"month":"06","publisher":"Association for Computing Machinery","day":"23","oa":1,"corr_author":"1","fulldoi":"https://doi.org/10.1145/3585391","arxiv":1,"date_published":"2023-06-23T00:00:00Z","file_date_updated":"2024-01-16T08:11:24Z","has_accepted_license":"1","keyword":["Theoretical Computer Science","Software"],"article_processing_charge":"Yes","year":"2023","quality_controlled":"1","publication_status":"published","intvolume":"        35","tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"ddc":["000"],"language":[{"iso":"eng"}],"acknowledgement":"This research was partially supported by the ERC CoG (grant no. 863818; ForM-SMArt), the Czech Science Foundation (grant no. GA21-24711S), and the European Union’s Horizon 2020 research and innovation program under the Marie Skłodowska-Curie Grant Agreement No. 665385.","ec_funded":1,"publication_identifier":{"issn":["0934-5043"],"eissn":["1433-299X"]},"publication":"Formal Aspects of Computing","issue":"2","scopus_import":"1","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","date_updated":"2025-09-09T14:19:27Z","related_material":{"record":[{"status":"public","relation":"earlier_version","id":"10414"}]},"project":[{"_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","name":"International IST Doctoral Program"}],"citation":{"chicago":"Chatterjee, Krishnendu, Ehsan Kafshdar Goharshady, Petr Novotný, Jiří Zárevúcky, and Dorde Zikelic. “On Lexicographic Proof Rules for Probabilistic Termination.” <i>Formal Aspects of Computing</i>. Association for Computing Machinery, 2023. <a href=\"https://doi.org/10.1145/3585391\">https://doi.org/10.1145/3585391</a>.","apa":"Chatterjee, K., Kafshdar Goharshady, E., Novotný, P., Zárevúcky, J., &#38; Zikelic, D. (2023). On lexicographic proof rules for probabilistic termination. <i>Formal Aspects of Computing</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3585391\">https://doi.org/10.1145/3585391</a>","mla":"Chatterjee, Krishnendu, et al. “On Lexicographic Proof Rules for Probabilistic Termination.” <i>Formal Aspects of Computing</i>, vol. 35, no. 2, 11, Association for Computing Machinery, 2023, doi:<a href=\"https://doi.org/10.1145/3585391\">10.1145/3585391</a>.","ama":"Chatterjee K, Kafshdar Goharshady E, Novotný P, Zárevúcky J, Zikelic D. On lexicographic proof rules for probabilistic termination. <i>Formal Aspects of Computing</i>. 2023;35(2). doi:<a href=\"https://doi.org/10.1145/3585391\">10.1145/3585391</a>","short":"K. Chatterjee, E. Kafshdar Goharshady, P. Novotný, J. Zárevúcky, D. Zikelic, Formal Aspects of Computing 35 (2023).","ieee":"K. Chatterjee, E. Kafshdar Goharshady, P. Novotný, J. Zárevúcky, and D. Zikelic, “On lexicographic proof rules for probabilistic termination,” <i>Formal Aspects of Computing</i>, vol. 35, no. 2. Association for Computing Machinery, 2023.","ista":"Chatterjee K, Kafshdar Goharshady E, Novotný P, Zárevúcky J, Zikelic D. 2023. On lexicographic proof rules for probabilistic termination. Formal Aspects of Computing. 35(2), 11."},"article_type":"original","oa_version":"Published Version","type":"journal_article","abstract":[{"text":"We consider the almost-sure (a.s.) termination problem for probabilistic programs, which are a stochastic extension of classical imperative programs. Lexicographic ranking functions provide a sound and practical approach for termination of non-probabilistic programs, and their extension to probabilistic programs is achieved via lexicographic ranking supermartingales (LexRSMs). However, LexRSMs introduced in the previous work have a limitation that impedes their automation: all of their components have to be non-negative in all reachable states. This might result in a LexRSM not existing even for simple terminating programs. Our contributions are twofold. First, we introduce a generalization of LexRSMs that allows for some components to be negative. This standard feature of non-probabilistic termination proofs was hitherto not known to be sound in the probabilistic setting, as the soundness proof requires a careful analysis of the underlying stochastic process. Second, we present polynomial-time algorithms using our generalized LexRSMs for proving a.s. termination in broad classes of linear-arithmetic programs.","lang":"eng"}],"_id":"14778","title":"On lexicographic proof rules for probabilistic termination","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Ehsan","last_name":"Kafshdar Goharshady","full_name":"Kafshdar Goharshady, Ehsan"},{"last_name":"Novotný","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotný, Petr"},{"full_name":"Zárevúcky, Jiří","last_name":"Zárevúcky","first_name":"Jiří"},{"orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","last_name":"Zikelic","first_name":"Dorde"}],"date_created":"2024-01-10T09:27:43Z","status":"public"},{"date_updated":"2025-04-15T06:25:30Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","fulldoi":"https://doi.org/10.1145/3410304","main_file_link":[{"open_access":"1","url":"https://doi.org/10.1145/3410304"}],"has_accepted_license":"1","date_published":"2021-06-01T00:00:00Z","related_material":{"record":[{"id":"9644","relation":"used_in_publication","status":"public"}]},"citation":{"ama":"Chatterjee K, Goharshady EK, Novotný P, Zikelic D. RevTerm. 2021. doi:<a href=\"https://doi.org/10.1145/3410304\">10.1145/3410304</a>","mla":"Chatterjee, Krishnendu, et al. <i>RevTerm</i>. Association for Computing Machinery, 2021, doi:<a href=\"https://doi.org/10.1145/3410304\">10.1145/3410304</a>.","short":"K. Chatterjee, E.K. Goharshady, P. Novotný, D. Zikelic, (2021).","ieee":"K. Chatterjee, E. K. Goharshady, P. Novotný, and D. Zikelic, “RevTerm.” Association for Computing Machinery, 2021.","ista":"Chatterjee K, Goharshady EK, Novotný P, Zikelic D. 2021. RevTerm, Association for Computing Machinery, <a href=\"https://doi.org/10.1145/3410304\">10.1145/3410304</a>.","chicago":"Chatterjee, Krishnendu, Ehsan Kafshdar Goharshady, Petr Novotný, and Dorde Zikelic. “RevTerm.” Association for Computing Machinery, 2021. <a href=\"https://doi.org/10.1145/3410304\">https://doi.org/10.1145/3410304</a>.","apa":"Chatterjee, K., Goharshady, E. K., Novotný, P., &#38; Zikelic, D. (2021). RevTerm. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3410304\">https://doi.org/10.1145/3410304</a>"},"article_processing_charge":"No","oa_version":"Published Version","type":"research_data_reference","year":"2021","abstract":[{"lang":"eng","text":"RevTerm is a static analysis tool for proving non-termination of integer C programs (possibly with non-determinism). RevTerm is an implementation of our method for non-termination proving presented in the paper “Proving Non-termination by Program Reversal”.\r\n\r\n"}],"title":"RevTerm","_id":"15284","ddc":["000"],"status":"public","date_created":"2024-04-03T09:00:42Z","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"first_name":"Ehsan Kafshdar","last_name":"Goharshady","full_name":"Goharshady, Ehsan Kafshdar"},{"id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","last_name":"Novotný","first_name":"Petr","full_name":"Novotný, Petr"},{"full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","first_name":"Dorde","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"}],"doi":"10.1145/3410304","publisher":"Association for Computing Machinery","month":"06","department":[{"_id":"KrCh"}],"day":"01","oa":1,"corr_author":"1"},{"department":[{"_id":"KrCh"}],"month":"11","publisher":"Springer Nature","external_id":{"isi":["000758218600033"],"arxiv":["2108.02188"]},"oa":1,"day":"10","doi":"10.1007/978-3-030-90870-6_33","volume":13047,"isi":1,"intvolume":"     13047","quality_controlled":"1","year":"2021","publication_status":"published","arxiv":1,"main_file_link":[{"url":"https://arxiv.org/abs/2108.02188","open_access":"1"}],"fulldoi":"https://doi.org/10.1007/978-3-030-90870-6_33","article_processing_charge":"No","alternative_title":["LNCS"],"date_published":"2021-11-10T00:00:00Z","conference":{"end_date":"2021-11-26","start_date":"2021-11-20","name":"FM: Formal Methods","location":"Virtual"},"publication_identifier":{"eissn":["1611-3349"],"isbn":["9-783-0309-0869-0"],"eisbn":["978-3-030-90870-6"],"issn":["0302-9743"]},"acknowledgement":"This research was partially supported by the ERC CoG 863818 (ForM-SMArt), the Czech Science Foundation grant No. GJ19-15134Y, and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","ec_funded":1,"scopus_import":"1","publication":"24th International Symposium on Formal Methods","language":[{"iso":"eng"}],"abstract":[{"text":"We consider the almost-sure (a.s.) termination problem for probabilistic programs, which are a stochastic extension of classical imperative programs. Lexicographic ranking functions provide a sound and practical approach for termination of non-probabilistic programs, and their extension to probabilistic programs is achieved via lexicographic ranking supermartingales (LexRSMs). However, LexRSMs introduced in the previous work have a limitation that impedes their automation: all of their components have to be non-negative in all reachable states. This might result in LexRSM not existing even for simple terminating programs. Our contributions are twofold: First, we introduce a generalization of LexRSMs which allows for some components to be negative. This standard feature of non-probabilistic termination proofs was hitherto not known to be sound in the probabilistic setting, as the soundness proof requires a careful analysis of the underlying stochastic process. Second, we present polynomial-time algorithms using our generalized LexRSMs for proving a.s. termination in broad classes of linear-arithmetic programs.","lang":"eng"}],"oa_version":"Preprint","type":"conference","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"full_name":"Kafshdar Goharshadi, Ehsan","orcid":"0000-0002-8595-0587","id":"103b4fa0-896a-11ed-bdf8-87b697bef40d","last_name":"Kafshdar Goharshadi","first_name":"Ehsan"},{"full_name":"Novotný, Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","last_name":"Novotný","first_name":"Petr"},{"last_name":"Zárevúcky","first_name":"Jiří","full_name":"Zárevúcky, Jiří"},{"full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","last_name":"Zikelic","first_name":"Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87"}],"date_created":"2021-12-05T23:01:45Z","status":"public","_id":"10414","title":"On lexicographic proof rules for probabilistic termination","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2026-04-07T13:27:55Z","project":[{"call_identifier":"H2020","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"},{"name":"International IST Doctoral Program","call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","grant_number":"665385"}],"citation":{"chicago":"Chatterjee, Krishnendu, Ehsan Goharshady, Petr Novotný, Jiří Zárevúcky, and Dorde Zikelic. “On Lexicographic Proof Rules for Probabilistic Termination.” In <i>24th International Symposium on Formal Methods</i>, 13047:619–39. Springer Nature, 2021. <a href=\"https://doi.org/10.1007/978-3-030-90870-6_33\">https://doi.org/10.1007/978-3-030-90870-6_33</a>.","apa":"Chatterjee, K., Goharshady, E., Novotný, P., Zárevúcky, J., &#38; Zikelic, D. (2021). On lexicographic proof rules for probabilistic termination. In <i>24th International Symposium on Formal Methods</i> (Vol. 13047, pp. 619–639). Virtual: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-90870-6_33\">https://doi.org/10.1007/978-3-030-90870-6_33</a>","ama":"Chatterjee K, Goharshady E, Novotný P, Zárevúcky J, Zikelic D. On lexicographic proof rules for probabilistic termination. In: <i>24th International Symposium on Formal Methods</i>. Vol 13047. Springer Nature; 2021:619-639. doi:<a href=\"https://doi.org/10.1007/978-3-030-90870-6_33\">10.1007/978-3-030-90870-6_33</a>","mla":"Chatterjee, Krishnendu, et al. “On Lexicographic Proof Rules for Probabilistic Termination.” <i>24th International Symposium on Formal Methods</i>, vol. 13047, Springer Nature, 2021, pp. 619–39, doi:<a href=\"https://doi.org/10.1007/978-3-030-90870-6_33\">10.1007/978-3-030-90870-6_33</a>.","ista":"Chatterjee K, Goharshady E, Novotný P, Zárevúcky J, Zikelic D. 2021. On lexicographic proof rules for probabilistic termination. 24th International Symposium on Formal Methods. FM: Formal Methods, LNCS, vol. 13047, 619–639.","short":"K. Chatterjee, E. Goharshady, P. Novotný, J. Zárevúcky, D. Zikelic, in:, 24th International Symposium on Formal Methods, Springer Nature, 2021, pp. 619–639.","ieee":"K. Chatterjee, E. Goharshady, P. Novotný, J. Zárevúcky, and D. Zikelic, “On lexicographic proof rules for probabilistic termination,” in <i>24th International Symposium on Formal Methods</i>, Virtual, 2021, vol. 13047, pp. 619–639."},"page":"619-639","related_material":{"record":[{"status":"public","relation":"later_version","id":"14778"},{"status":"public","id":"14539","relation":"dissertation_contains"}]}},{"fulldoi":"https://doi.org/10.1145/3453483.3454093","arxiv":1,"main_file_link":[{"url":"https://arxiv.org/abs/2104.01189","open_access":"1"}],"date_published":"2021-06-01T00:00:00Z","conference":{"location":"Online","start_date":"2021-06-20","end_date":"2021-06-26","name":"PLDI: Programming Language Design and Implementation"},"article_processing_charge":"No","year":"2021","quality_controlled":"1","publication_status":"published","doi":"10.1145/3453483.3454093","isi":1,"external_id":{"arxiv":["2104.01189"],"isi":["000723661700067"]},"department":[{"_id":"KrCh"}],"month":"06","publisher":"Association for Computing Machinery","day":"01","oa":1,"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","date_updated":"2026-04-07T13:27:55Z","related_material":{"record":[{"status":"public","relation":"research_data","id":"15284"},{"relation":"dissertation_contains","id":"14539","status":"public"}]},"project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818"}],"page":"1033-1048","citation":{"ista":"Chatterjee K, Goharshady EK, Novotný P, Zikelic D. 2021. Proving non-termination by program reversal. Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. PLDI: Programming Language Design and Implementation, 1033–1048.","ieee":"K. Chatterjee, E. K. Goharshady, P. Novotný, and D. Zikelic, “Proving non-termination by program reversal,” in <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, Online, 2021, pp. 1033–1048.","short":"K. Chatterjee, E.K. Goharshady, P. Novotný, D. Zikelic, in:, Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2021, pp. 1033–1048.","mla":"Chatterjee, Krishnendu, et al. “Proving Non-Termination by Program Reversal.” <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, Association for Computing Machinery, 2021, pp. 1033–48, doi:<a href=\"https://doi.org/10.1145/3453483.3454093\">10.1145/3453483.3454093</a>.","ama":"Chatterjee K, Goharshady EK, Novotný P, Zikelic D. Proving non-termination by program reversal. In: <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>. Association for Computing Machinery; 2021:1033-1048. doi:<a href=\"https://doi.org/10.1145/3453483.3454093\">10.1145/3453483.3454093</a>","apa":"Chatterjee, K., Goharshady, E. K., Novotný, P., &#38; Zikelic, D. (2021). Proving non-termination by program reversal. In <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i> (pp. 1033–1048). Online: Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3453483.3454093\">https://doi.org/10.1145/3453483.3454093</a>","chicago":"Chatterjee, Krishnendu, Ehsan Kafshdar Goharshady, Petr Novotný, and Dorde Zikelic. “Proving Non-Termination by Program Reversal.” In <i>Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation</i>, 1033–48. Association for Computing Machinery, 2021. <a href=\"https://doi.org/10.1145/3453483.3454093\">https://doi.org/10.1145/3453483.3454093</a>."},"type":"conference","oa_version":"Preprint","abstract":[{"lang":"eng","text":"We present a new approach to proving non-termination of non-deterministic integer programs. Our technique is rather simple but efficient. It relies on a purely syntactic reversal of the program's transition system followed by a constraint-based invariant synthesis with constraints coming from both the original and the reversed transition system. The latter task is performed by a simple call to an off-the-shelf SMT-solver, which allows us to leverage the latest advances in SMT-solving. Moreover, our method offers a combination of features not present (as a whole) in previous approaches: it handles programs with non-determinism, provides relative completeness guarantees and supports programs with polynomial arithmetic. The experiments performed with our prototype tool RevTerm show that our approach, despite its simplicity and stronger theoretical guarantees, is at least on par with the state-of-the-art tools, often achieving a non-trivial improvement under a proper configuration of its parameters."}],"_id":"9644","title":"Proving non-termination by program reversal","status":"public","date_created":"2021-07-11T22:01:17Z","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Goharshady","first_name":"Ehsan Kafshdar","full_name":"Goharshady, Ehsan Kafshdar"},{"first_name":"Petr","last_name":"Novotný","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotný, Petr"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","last_name":"Zikelic","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde"}],"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["9781450383912"]},"ec_funded":1,"acknowledgement":"We thank the anonymous reviewers for their helpful comments. This research was partially supported by the ERCCoG 863818 (ForM-SMArt) and the Czech Science Foundation grant No. GJ19-15134Y.","publication":"Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","scopus_import":"1"},{"file":[{"date_updated":"2025-09-23T12:03:09Z","content_type":"application/pdf","file_name":"2020_ProbProgramming_Chatterjee.pdf","file_size":316681,"file_id":"20380","access_level":"open_access","relation":"main_file","creator":"dernst","success":1,"date_created":"2025-09-23T12:03:09Z","checksum":"28ece115e8d2d9263e253a598e7caef2"}],"doi":"10.1017/9781108770750.008","day":"18","oa":1,"corr_author":"1","department":[{"_id":"KrCh"}],"month":"11","publisher":"Cambridge University Press","date_published":"2020-11-18T00:00:00Z","file_date_updated":"2025-09-23T12:03:09Z","has_accepted_license":"1","article_processing_charge":"No","fulldoi":"https://doi.org/10.1017/9781108770750.008","ddc":["000"],"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"year":"2020","quality_controlled":"1","publication_status":"published","OA_place":"publisher","language":[{"iso":"eng"}],"publication":"Foundations of Probabilistic Programming","publication_identifier":{"isbn":["9781108488518"],"eisbn":["9781108770750"]},"acknowledgement":"Krishnendu Chatterjee is supported by the Austrian Science Fund (FWF) NFN\r\nGrant No. S11407-N23 (RiSE/SHiNE), and COST Action GAMENET. Hongfei Fu\r\nis supported by the National Natural Science Foundation of China (NSFC) Grant\r\nNo. 61802254. Petr Novotný is supported by the Czech Science Foundation grant\r\nNo. GJ19-15134Y.","project":[{"name":"Game Theory","call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407"}],"citation":{"apa":"Chatterjee, K., Fu, H., &#38; Novotný, P. (2020). Termination Analysis of Probabilistic Programs with Martingales. In <i>Foundations of Probabilistic Programming</i> (pp. 221–258). Cambridge University Press. <a href=\"https://doi.org/10.1017/9781108770750.008\">https://doi.org/10.1017/9781108770750.008</a>","chicago":"Chatterjee, Krishnendu, Hongfei Fu, and Petr Novotný. “Termination Analysis of Probabilistic Programs with Martingales.” In <i>Foundations of Probabilistic Programming</i>, 221–58. Cambridge University Press, 2020. <a href=\"https://doi.org/10.1017/9781108770750.008\">https://doi.org/10.1017/9781108770750.008</a>.","ieee":"K. Chatterjee, H. Fu, and P. Novotný, “Termination Analysis of Probabilistic Programs with Martingales,” in <i>Foundations of Probabilistic Programming</i>, Cambridge University Press, 2020, pp. 221–258.","short":"K. Chatterjee, H. Fu, P. Novotný, in:, Foundations of Probabilistic Programming, Cambridge University Press, 2020, pp. 221–258.","ista":"Chatterjee K, Fu H, Novotný P. 2020.Termination Analysis of Probabilistic Programs with Martingales. In: Foundations of Probabilistic Programming. , 221–258.","mla":"Chatterjee, Krishnendu, et al. “Termination Analysis of Probabilistic Programs with Martingales.” <i>Foundations of Probabilistic Programming</i>, Cambridge University Press, 2020, pp. 221–58, doi:<a href=\"https://doi.org/10.1017/9781108770750.008\">10.1017/9781108770750.008</a>.","ama":"Chatterjee K, Fu H, Novotný P. Termination Analysis of Probabilistic Programs with Martingales. In: <i>Foundations of Probabilistic Programming</i>. Cambridge University Press; 2020:221-258. doi:<a href=\"https://doi.org/10.1017/9781108770750.008\">10.1017/9781108770750.008</a>"},"page":"221-258","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2025-09-23T12:10:25Z","_id":"19986","title":"Termination Analysis of Probabilistic Programs with Martingales","status":"public","date_created":"2025-07-10T13:28:51Z","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","first_name":"Hongfei","last_name":"Fu","full_name":"Fu, Hongfei"},{"last_name":"Novotný","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotný, Petr"}],"type":"book_chapter","oa_version":"Published Version","abstract":[{"lang":"eng","text":"For non-probabilistic programs, a key question in static analysis is termination, which asks whether a given program terminates under a given initial condition. In the presence of probabilistic behaviour, there are two fundamental extensions of the termination question: (a) the almost-sure termination question, which asks whether the termination probability is 1; and (b) the bounded-time termination question, which asks whether the expected termination time is bounded. There are many active research directions to address these two questions; one important such direction is the use of martingale theory for termination analysis. In this chapter, we survey the main techniques of the martingale-based approach to the termination analysis of probabilistic programs."}]},{"acknowledgement":"Krishnendu Chatterjee is supported by the Austrian ScienceFund (FWF) NFN Grant No. S11407-N23 (RiSE/SHiNE),and COST Action GAMENET. Petr Novotn ́y is supported bythe Czech Science Foundation grant No. GJ19-15134Y.","publication_identifier":{"eissn":["2334-0843"],"issn":["2334-0835"]},"publication":"Proceedings of the 30th International Conference on Automated Planning and Scheduling","scopus_import":"1","language":[{"iso":"eng"}],"oa_version":"None","type":"conference","abstract":[{"lang":"eng","text":"Multiple-environment Markov decision processes (MEMDPs) are MDPs equipped with not one, but multiple probabilistic transition functions, which represent the various possible unknown environments. While the previous research on MEMDPs focused on theoretical properties for long-run average payoff, we study them with discounted-sum payoff and focus on their practical advantages and applications. MEMDPs can be viewed as a special case of Partially observable and Mixed observability MDPs: the state of the system is perfectly observable, but not the environment. We show that the specific structure of MEMDPs allows for more efficient algorithmic analysis, in particular for faster belief updates. We demonstrate the applicability of MEMDPs in several domains. In particular, we formalize the sequential decision-making approach to contextual recommendation systems as MEMDPs and substantially improve over the previous MDP approach."}],"title":"Multiple-environment Markov decision processes: Efficient analysis and applications","_id":"8193","status":"public","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Chmelik, Martin","first_name":"Martin","last_name":"Chmelik","id":"3624234E-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Karkhanis, Deep","first_name":"Deep","last_name":"Karkhanis"},{"last_name":"Novotný","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotný, Petr"},{"last_name":"Royer","first_name":"Amélie","id":"3811D890-F248-11E8-B48F-1D18A9856A87","full_name":"Royer, Amélie","orcid":"0000-0002-8407-0705"}],"date_created":"2020-08-02T22:00:58Z","date_updated":"2026-04-08T07:26:44Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"status":"public","id":"8390","relation":"dissertation_contains"}]},"page":"48-56","citation":{"ista":"Chatterjee K, Chmelik M, Karkhanis D, Novotný P, Royer A. 2020. Multiple-environment Markov decision processes: Efficient analysis and applications. Proceedings of the 30th International Conference on Automated Planning and Scheduling. ICAPS: International Conference on Automated Planning and Scheduling vol. 30, 48–56.","short":"K. Chatterjee, M. Chmelik, D. Karkhanis, P. Novotný, A. Royer, in:, Proceedings of the 30th International Conference on Automated Planning and Scheduling, Association for the Advancement of Artificial Intelligence, 2020, pp. 48–56.","ieee":"K. Chatterjee, M. Chmelik, D. Karkhanis, P. Novotný, and A. Royer, “Multiple-environment Markov decision processes: Efficient analysis and applications,” in <i>Proceedings of the 30th International Conference on Automated Planning and Scheduling</i>, Nancy, France, 2020, vol. 30, pp. 48–56.","mla":"Chatterjee, Krishnendu, et al. “Multiple-Environment Markov Decision Processes: Efficient Analysis and Applications.” <i>Proceedings of the 30th International Conference on Automated Planning and Scheduling</i>, vol. 30, Association for the Advancement of Artificial Intelligence, 2020, pp. 48–56.","ama":"Chatterjee K, Chmelik M, Karkhanis D, Novotný P, Royer A. Multiple-environment Markov decision processes: Efficient analysis and applications. In: <i>Proceedings of the 30th International Conference on Automated Planning and Scheduling</i>. Vol 30. Association for the Advancement of Artificial Intelligence; 2020:48-56.","apa":"Chatterjee, K., Chmelik, M., Karkhanis, D., Novotný, P., &#38; Royer, A. (2020). Multiple-environment Markov decision processes: Efficient analysis and applications. In <i>Proceedings of the 30th International Conference on Automated Planning and Scheduling</i> (Vol. 30, pp. 48–56). Nancy, France: Association for the Advancement of Artificial Intelligence.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, Deep Karkhanis, Petr Novotný, and Amélie Royer. “Multiple-Environment Markov Decision Processes: Efficient Analysis and Applications.” In <i>Proceedings of the 30th International Conference on Automated Planning and Scheduling</i>, 30:48–56. Association for the Advancement of Artificial Intelligence, 2020."},"project":[{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory","grant_number":"S11407"}],"publisher":"Association for the Advancement of Artificial Intelligence","department":[{"_id":"KrCh"}],"month":"06","day":"01","volume":30,"publication_status":"published","quality_controlled":"1","year":"2020","intvolume":"        30","conference":{"location":"Nancy, France","end_date":"2020-10-30","start_date":"2020-10-26","name":"ICAPS: International Conference on Automated Planning and Scheduling"},"date_published":"2020-06-01T00:00:00Z","article_processing_charge":"No"},{"volume":11781,"doi":"10.1007/978-3-030-31784-3_27","isi":1,"external_id":{"arxiv":["1907.11010"],"isi":["000723515700027"]},"month":"10","department":[{"_id":"KrCh"}],"publisher":"Springer Nature","day":"21","oa":1,"fulldoi":"https://doi.org/10.1007/978-3-030-31784-3_27","arxiv":1,"main_file_link":[{"url":"https://arxiv.org/abs/1907.11010","open_access":"1"}],"alternative_title":["LNCS"],"date_published":"2019-10-21T00:00:00Z","conference":{"name":"ATVA: Automated TEchnology for Verification and Analysis","end_date":"2019-10-31","start_date":"2019-10-28","location":"Taipei, Taiwan"},"article_processing_charge":"No","quality_controlled":"1","year":"2019","publication_status":"published","intvolume":"     11781","language":[{"iso":"eng"}],"publication_identifier":{"eissn":["1611-3349"],"isbn":["9783030317836"],"issn":["0302-9743"]},"publication":"International Symposium on Automated Technology for Verification and Analysis","scopus_import":"1","user_id":"ba8df636-2132-11f1-aed0-ed93e2281fdd","date_updated":"2026-04-16T09:51:24Z","project":[{"grant_number":"S 11407_N23","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF"}],"citation":{"short":"T. Brázdil, K. Chatterjee, A. Kucera, P. Novotný, D. Velan, in:, International Symposium on Automated Technology for Verification and Analysis, Springer Nature, 2019, pp. 462–478.","ieee":"T. Brázdil, K. Chatterjee, A. Kucera, P. Novotný, and D. Velan, “Deciding fast termination for probabilistic VASS with nondeterminism,” in <i>International Symposium on Automated Technology for Verification and Analysis</i>, Taipei, Taiwan, 2019, vol. 11781, pp. 462–478.","ista":"Brázdil T, Chatterjee K, Kucera A, Novotný P, Velan D. 2019. Deciding fast termination for probabilistic VASS with nondeterminism. International Symposium on Automated Technology for Verification and Analysis. ATVA: Automated TEchnology for Verification and Analysis, LNCS, vol. 11781, 462–478.","mla":"Brázdil, Tomás, et al. “Deciding Fast Termination for Probabilistic VASS with Nondeterminism.” <i>International Symposium on Automated Technology for Verification and Analysis</i>, vol. 11781, Springer Nature, 2019, pp. 462–78, doi:<a href=\"https://doi.org/10.1007/978-3-030-31784-3_27\">10.1007/978-3-030-31784-3_27</a>.","ama":"Brázdil T, Chatterjee K, Kucera A, Novotný P, Velan D. Deciding fast termination for probabilistic VASS with nondeterminism. In: <i>International Symposium on Automated Technology for Verification and Analysis</i>. Vol 11781. Springer Nature; 2019:462-478. doi:<a href=\"https://doi.org/10.1007/978-3-030-31784-3_27\">10.1007/978-3-030-31784-3_27</a>","apa":"Brázdil, T., Chatterjee, K., Kucera, A., Novotný, P., &#38; Velan, D. (2019). Deciding fast termination for probabilistic VASS with nondeterminism. In <i>International Symposium on Automated Technology for Verification and Analysis</i> (Vol. 11781, pp. 462–478). Taipei, Taiwan: Springer Nature. <a href=\"https://doi.org/10.1007/978-3-030-31784-3_27\">https://doi.org/10.1007/978-3-030-31784-3_27</a>","chicago":"Brázdil, Tomás, Krishnendu Chatterjee, Antonín Kucera, Petr Novotný, and Dominik Velan. “Deciding Fast Termination for Probabilistic VASS with Nondeterminism.” In <i>International Symposium on Automated Technology for Verification and Analysis</i>, 11781:462–78. Springer Nature, 2019. <a href=\"https://doi.org/10.1007/978-3-030-31784-3_27\">https://doi.org/10.1007/978-3-030-31784-3_27</a>."},"page":"462-478","type":"conference","oa_version":"Preprint","abstract":[{"lang":"eng","text":"A probabilistic vector addition system with states (pVASS) is a finite state Markov process augmented with non-negative integer counters that can be incremented or decremented during each state transition, blocking any behaviour that would cause a counter to decrease below zero. The pVASS can be used as abstractions of probabilistic programs with many decidable properties. The use of pVASS as abstractions requires the presence of nondeterminism in the model. In this paper, we develop techniques for checking fast termination of pVASS with nondeterminism. That is, for every initial configuration of size n, we consider the worst expected number of transitions needed to reach a configuration with some counter negative (the expected termination time). We show that the problem whether the asymptotic expected termination time is linear is decidable in polynomial time for a certain natural class of pVASS with nondeterminism. Furthermore, we show the following dichotomy: if the asymptotic expected termination time is not linear, then it is at least quadratic, i.e., in Ω(n2)."}],"_id":"7183","title":"Deciding fast termination for probabilistic VASS with nondeterminism","author":[{"first_name":"Tomás","last_name":"Brázdil","full_name":"Brázdil, Tomás"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"last_name":"Kucera","first_name":"Antonín","full_name":"Kucera, Antonín"},{"last_name":"Novotný","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotný, Petr"},{"full_name":"Velan, Dominik","first_name":"Dominik","last_name":"Velan"}],"status":"public","date_created":"2019-12-15T23:00:44Z"},{"oa":1,"day":"01","month":"07","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"publisher":"IJCAI","external_id":{"isi":["000764175404117"],"arxiv":["1804.10601"]},"isi":1,"doi":"10.24963/ijcai.2018/652","volume":2018,"intvolume":"      2018","quality_controlled":"1","year":"2018","publication_status":"published","article_processing_charge":"No","date_published":"2018-07-01T00:00:00Z","conference":{"location":"Stockholm, Sweden","start_date":"2018-07-13","end_date":"2018-07-19","name":"IJCAI: International Joint Conference on Artificial Intelligence"},"arxiv":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1804.10601"}],"fulldoi":"https://doi.org/10.24963/ijcai.2018/652","scopus_import":"1","acknowledgement":"This research was supported by the Vienna Science and Technology Fund (WWTF) grant ICT15-003; Austrian Science Fund (FWF): S11407-N23(RiSE/SHiNE);and an ERC Start Grant (279307:Graph Games).\r\n","ec_funded":1,"language":[{"iso":"eng"}],"publist_id":"8031","status":"public","date_created":"2018-12-11T11:44:13Z","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Adrian","last_name":"Elgyütt","id":"4A2E9DBA-F248-11E8-B48F-1D18A9856A87","full_name":"Elgyütt, Adrian"},{"first_name":"Petr","last_name":"Novotny","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotny, Petr"},{"full_name":"Rouillé, Owen","last_name":"Rouillé","first_name":"Owen"}],"_id":"24","title":"Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum objectives","abstract":[{"lang":"eng","text":"Partially-observable Markov decision processes (POMDPs) with discounted-sum payoff are a standard framework to model a wide range of problems related to decision making under uncertainty. Traditionally, the goal has been to obtain policies that optimize the expectation of the discounted-sum payoff. A key drawback of the expectation measure is that even low probability events with extreme payoff can significantly affect the expectation, and thus the obtained policies are not necessarily risk-averse. An alternate approach is to optimize the probability that the payoff is above a certain threshold, which allows obtaining risk-averse policies, but ignores optimization of the expectation. We consider the expectation optimization with probabilistic guarantee (EOPG) problem, where the goal is to optimize the expectation ensuring that the payoff is above a given threshold with at least a specified probability. We present several results on the EOPG problem, including the first algorithm to solve it."}],"oa_version":"Preprint","type":"conference","project":[{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"}],"citation":{"ama":"Chatterjee K, Elgyütt A, Novotný P, Rouillé O. Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum objectives. In: Vol 2018. IJCAI; 2018:4692-4699. doi:<a href=\"https://doi.org/10.24963/ijcai.2018/652\">10.24963/ijcai.2018/652</a>","mla":"Chatterjee, Krishnendu, et al. <i>Expectation Optimization with Probabilistic Guarantees in POMDPs with Discounted-Sum Objectives</i>. Vol. 2018, IJCAI, 2018, pp. 4692–99, doi:<a href=\"https://doi.org/10.24963/ijcai.2018/652\">10.24963/ijcai.2018/652</a>.","ieee":"K. Chatterjee, A. Elgyütt, P. Novotný, and O. Rouillé, “Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum objectives,” presented at the IJCAI: International Joint Conference on Artificial Intelligence, Stockholm, Sweden, 2018, vol. 2018, pp. 4692–4699.","short":"K. Chatterjee, A. Elgyütt, P. Novotný, O. Rouillé, in:, IJCAI, 2018, pp. 4692–4699.","ista":"Chatterjee K, Elgyütt A, Novotný P, Rouillé O. 2018. Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum objectives. IJCAI: International Joint Conference on Artificial Intelligence vol. 2018, 4692–4699.","chicago":"Chatterjee, Krishnendu, Adrian Elgyütt, Petr Novotný, and Owen Rouillé. “Expectation Optimization with Probabilistic Guarantees in POMDPs with Discounted-Sum Objectives,” 2018:4692–99. IJCAI, 2018. <a href=\"https://doi.org/10.24963/ijcai.2018/652\">https://doi.org/10.24963/ijcai.2018/652</a>.","apa":"Chatterjee, K., Elgyütt, A., Novotný, P., &#38; Rouillé, O. (2018). Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum objectives (Vol. 2018, pp. 4692–4699). Presented at the IJCAI: International Joint Conference on Artificial Intelligence, Stockholm, Sweden: IJCAI. <a href=\"https://doi.org/10.24963/ijcai.2018/652\">https://doi.org/10.24963/ijcai.2018/652</a>"},"page":"4692 - 4699","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","date_updated":"2025-04-14T13:51:04Z"},{"publist_id":"7780","language":[{"iso":"eng"}],"publication_identifier":{"isbn":["978-1-4503-5583-4"]},"ec_funded":1,"scopus_import":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2025-06-04T08:04:55Z","project":[{"grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425","name":"Efficient Algorithms for Computer Aided Verification"},{"grant_number":"279307","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","call_identifier":"FWF","grant_number":"S 11407_N23"}],"citation":{"ieee":"T. Brázdil, K. Chatterjee, A. Kučera, P. Novotný, D. Velan, and F. Zuleger, “Efficient algorithms for asymptotic bounds on termination time in VASS,” presented at the LICS: Logic in Computer Science, Oxford, United Kingdom, 2018, vol. F138033, pp. 185–194.","short":"T. Brázdil, K. Chatterjee, A. Kučera, P. Novotný, D. Velan, F. Zuleger, in:, IEEE, 2018, pp. 185–194.","ista":"Brázdil T, Chatterjee K, Kučera A, Novotný P, Velan D, Zuleger F. 2018. Efficient algorithms for asymptotic bounds on termination time in VASS. LICS: Logic in Computer Science, ACM/IEEE Symposium on Logic in Computer Science, vol. F138033, 185–194.","ama":"Brázdil T, Chatterjee K, Kučera A, Novotný P, Velan D, Zuleger F. Efficient algorithms for asymptotic bounds on termination time in VASS. In: Vol F138033. IEEE; 2018:185-194. doi:<a href=\"https://doi.org/10.1145/3209108.3209191\">10.1145/3209108.3209191</a>","mla":"Brázdil, Tomáš, et al. <i>Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS</i>. Vol. F138033, IEEE, 2018, pp. 185–94, doi:<a href=\"https://doi.org/10.1145/3209108.3209191\">10.1145/3209108.3209191</a>.","apa":"Brázdil, T., Chatterjee, K., Kučera, A., Novotný, P., Velan, D., &#38; Zuleger, F. (2018). Efficient algorithms for asymptotic bounds on termination time in VASS (Vol. F138033, pp. 185–194). Presented at the LICS: Logic in Computer Science, Oxford, United Kingdom: IEEE. <a href=\"https://doi.org/10.1145/3209108.3209191\">https://doi.org/10.1145/3209108.3209191</a>","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Antonín Kučera, Petr Novotný, Dominik Velan, and Florian Zuleger. “Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS,” F138033:185–94. IEEE, 2018. <a href=\"https://doi.org/10.1145/3209108.3209191\">https://doi.org/10.1145/3209108.3209191</a>."},"page":"185 - 194","oa_version":"Preprint","type":"conference","abstract":[{"lang":"eng","text":"Vector Addition Systems with States (VASS) provide a well-known and fundamental model for the analysis of concurrent processes, parameterized systems, and are also used as abstract models of programs in resource bound analysis. In this paper we study the problem of obtaining asymptotic bounds on the termination time of a given VASS. In particular, we focus on the practically important case of obtaining polynomial bounds on termination time. Our main contributions are as follows: First, we present a polynomial-time algorithm for deciding whether a given VASS has a linear asymptotic complexity. We also show that if the complexity of a VASS is not linear, it is at least quadratic. Second, we classify VASS according to quantitative properties of their cycles. We show that certain singularities in these properties are the key reason for non-polynomial asymptotic complexity of VASS. In absence of singularities, we show that the asymptotic complexity is always polynomial and of the form Θ(nk), for some integer k d, where d is the dimension of the VASS. We present a polynomial-time algorithm computing the optimal k. For general VASS, the same algorithm, which is based on a complete technique for the construction of ranking functions in VASS, produces a valid lower bound, i.e., a k such that the termination complexity is (nk). Our results are based on new insights into the geometry of VASS dynamics, which hold the potential for further applicability to VASS analysis."}],"_id":"143","title":"Efficient algorithms for asymptotic bounds on termination time in VASS","author":[{"full_name":"Brázdil, Tomáš","first_name":"Tomáš","last_name":"Brázdil"},{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Kučera","first_name":"Antonín","full_name":"Kučera, Antonín"},{"first_name":"Petr","last_name":"Novotny","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotny, Petr"},{"first_name":"Dominik","last_name":"Velan","full_name":"Velan, Dominik"},{"last_name":"Zuleger","first_name":"Florian","full_name":"Zuleger, Florian"}],"status":"public","date_created":"2018-12-11T11:44:51Z","volume":"F138033","doi":"10.1145/3209108.3209191","isi":1,"external_id":{"isi":["000545262800020"],"arxiv":["1804.10985"]},"month":"07","department":[{"_id":"KrCh"}],"publisher":"IEEE","day":"09","oa":1,"fulldoi":"https://doi.org/10.1145/3209108.3209191","arxiv":1,"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1804.10985"}],"date_published":"2018-07-09T00:00:00Z","alternative_title":["ACM/IEEE Symposium on Logic in Computer Science"],"conference":{"location":"Oxford, United Kingdom","name":"LICS: Logic in Computer Science","start_date":"2018-07-09","end_date":"2018-07-12"},"article_processing_charge":"No","year":"2018","quality_controlled":"1","publication_status":"published"},{"article_processing_charge":"No","date_published":"2018-06-01T00:00:00Z","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1510.08517"}],"arxiv":1,"fulldoi":"https://doi.org/10.1145/3174800","intvolume":"        40","publication_status":"published","year":"2018","quality_controlled":"1","isi":1,"article_number":"7","doi":"10.1145/3174800","volume":40,"oa":1,"day":"01","publisher":"Association for Computing Machinery","month":"06","department":[{"_id":"KrCh"}],"external_id":{"isi":["000434634500003"],"arxiv":["1510.08517"]},"citation":{"mla":"Chatterjee, Krishnendu, et al. “Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs.” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 40, no. 2, 7, Association for Computing Machinery, 2018, doi:<a href=\"https://doi.org/10.1145/3174800\">10.1145/3174800</a>.","ama":"Chatterjee K, Fu H, Novotný P, Hasheminezhad R. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. <i>ACM Transactions on Programming Languages and Systems</i>. 2018;40(2). doi:<a href=\"https://doi.org/10.1145/3174800\">10.1145/3174800</a>","ista":"Chatterjee K, Fu H, Novotný P, Hasheminezhad R. 2018. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. ACM Transactions on Programming Languages and Systems. 40(2), 7.","ieee":"K. Chatterjee, H. Fu, P. Novotný, and R. Hasheminezhad, “Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs,” <i>ACM Transactions on Programming Languages and Systems</i>, vol. 40, no. 2. Association for Computing Machinery, 2018.","short":"K. Chatterjee, H. Fu, P. Novotný, R. Hasheminezhad, ACM Transactions on Programming Languages and Systems 40 (2018).","chicago":"Chatterjee, Krishnendu, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad. “Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs.” <i>ACM Transactions on Programming Languages and Systems</i>. Association for Computing Machinery, 2018. <a href=\"https://doi.org/10.1145/3174800\">https://doi.org/10.1145/3174800</a>.","apa":"Chatterjee, K., Fu, H., Novotný, P., &#38; Hasheminezhad, R. (2018). Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. <i>ACM Transactions on Programming Languages and Systems</i>. Association for Computing Machinery. <a href=\"https://doi.org/10.1145/3174800\">https://doi.org/10.1145/3174800</a>"},"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","grant_number":"279307"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme","grant_number":"291734"}],"related_material":{"record":[{"status":"public","relation":"earlier_version","id":"1438"}]},"date_updated":"2025-04-15T08:12:22Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_created":"2019-02-14T12:29:10Z","status":"public","author":[{"last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"first_name":"Hongfei","last_name":"Fu","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","full_name":"Fu, Hongfei"},{"first_name":"Petr","last_name":"Novotný","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotný, Petr"},{"full_name":"Hasheminezhad, Rouzbeh","last_name":"Hasheminezhad","first_name":"Rouzbeh"}],"title":"Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs","_id":"5993","abstract":[{"text":"In this article, we consider the termination problem of probabilistic programs with real-valued variables. Thequestions concerned are: qualitative ones that ask (i) whether the program terminates with probability 1(almost-sure termination) and (ii) whether the expected termination time is finite (finite termination); andquantitative ones that ask (i) to approximate the expected termination time (expectation problem) and (ii) tocompute a boundBsuch that the probability not to terminate afterBsteps decreases exponentially (con-centration problem). To solve these questions, we utilize the notion of ranking supermartingales, which isa powerful approach for proving termination of probabilistic programs. In detail, we focus on algorithmicsynthesis of linear ranking-supermartingales over affine probabilistic programs (Apps) with both angelic anddemonic non-determinism. An important subclass of Apps is LRApp which is defined as the class of all Appsover which a linear ranking-supermartingale exists.Our main contributions are as follows. Firstly, we show that the membership problem of LRApp (i) canbe decided in polynomial time for Apps with at most demonic non-determinism, and (ii) isNP-hard and inPSPACEfor Apps with angelic non-determinism. Moreover, theNP-hardness result holds already for Appswithout probability and demonic non-determinism. Secondly, we show that the concentration problem overLRApp can be solved in the same complexity as for the membership problem of LRApp. Finally, we show thatthe expectation problem over LRApp can be solved in2EXPTIMEand isPSPACE-hard even for Apps withoutprobability and non-determinism (i.e., deterministic programs). Our experimental results demonstrate theeffectiveness of our approach to answer the qualitative and quantitative questions over Apps with at mostdemonic non-determinism.","lang":"eng"}],"type":"journal_article","oa_version":"Submitted Version","language":[{"iso":"eng"}],"scopus_import":"1","issue":"2","publication":"ACM Transactions on Programming Languages and Systems","publication_identifier":{"issn":["0164-0925"]},"ec_funded":1},{"citation":{"mla":"Agrawal, Sheshansh, et al. <i>Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs</i>. Vol. 2, no. POPL, 34, ACM, 2018, doi:<a href=\"https://doi.org/10.1145/3158122\">10.1145/3158122</a>.","ama":"Agrawal S, Chatterjee K, Novotný P. Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. In: Vol 2. ACM; 2018. doi:<a href=\"https://doi.org/10.1145/3158122\">10.1145/3158122</a>","ieee":"S. Agrawal, K. Chatterjee, and P. Novotný, “Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs,” presented at the POPL: Principles of Programming Languages, Los Angeles, CA, USA, 2018, vol. 2, no. POPL.","ista":"Agrawal S, Chatterjee K, Novotný P. 2018. Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. POPL: Principles of Programming Languages vol. 2, 34.","short":"S. Agrawal, K. Chatterjee, P. Novotný, in:, ACM, 2018.","chicago":"Agrawal, Sheshansh, Krishnendu Chatterjee, and Petr Novotný. “Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs,” Vol. 2. ACM, 2018. <a href=\"https://doi.org/10.1145/3158122\">https://doi.org/10.1145/3158122</a>.","apa":"Agrawal, S., Chatterjee, K., &#38; Novotný, P. (2018). Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs (Vol. 2). Presented at the POPL: Principles of Programming Languages, Los Angeles, CA, USA: ACM. <a href=\"https://doi.org/10.1145/3158122\">https://doi.org/10.1145/3158122</a>"},"project":[{"grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"date_updated":"2024-10-21T06:02:40Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","status":"public","date_created":"2018-12-11T11:45:50Z","author":[{"last_name":"Agrawal","first_name":"Sheshansh","full_name":"Agrawal, Sheshansh"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","first_name":"Krishnendu"},{"full_name":"Novotny, Petr","last_name":"Novotny","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"}],"title":"Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs","_id":"325","abstract":[{"text":"Probabilistic programs extend classical imperative programs with real-valued random variables and random branching. The most basic liveness property for such programs is the termination property. The qualitative (aka almost-sure) termination problem asks whether a given program program terminates with probability 1. While ranking functions provide a sound and complete method for non-probabilistic programs, the extension of them to probabilistic programs is achieved via ranking supermartingales (RSMs). Although deep theoretical results have been established about RSMs, their application to probabilistic programs with nondeterminism has been limited only to programs of restricted control-flow structure. For non-probabilistic programs, lexicographic ranking functions provide a compositional and practical approach for termination analysis of real-world programs. In this work we introduce lexicographic RSMs and show that they present a sound method for almost-sure termination of probabilistic programs with nondeterminism. We show that lexicographic RSMs provide a tool for compositional reasoning about almost-sure termination, and for probabilistic programs with linear arithmetic they can be synthesized efficiently (in polynomial time). We also show that with additional restrictions even asymptotic bounds on expected termination time can be obtained through lexicographic RSMs. Finally, we present experimental results on benchmarks adapted from previous work to demonstrate the effectiveness of our approach.","lang":"eng"}],"type":"conference","oa_version":"Preprint","language":[{"iso":"eng"}],"publist_id":"7540","scopus_import":"1","issue":"POPL","conference":{"start_date":"2018-01-07","end_date":"2018-01-13","name":"POPL: Principles of Programming Languages","location":"Los Angeles, CA, USA"},"date_published":"2018-01-01T00:00:00Z","main_file_link":[{"url":"https://arxiv.org/abs/1709.04037","open_access":"1"}],"arxiv":1,"fulldoi":"https://doi.org/10.1145/3158122","intvolume":"         2","publication_status":"published","year":"2018","quality_controlled":"1","article_number":"34","doi":"10.1145/3158122","volume":2,"oa":1,"day":"01","publisher":"ACM","department":[{"_id":"KrCh"}],"month":"01","external_id":{"arxiv":["1709.04037"]}},{"fulldoi":"https://doi.org/10.1145/3009837.3009873","main_file_link":[{"url":"https://arxiv.org/abs/1611.01063","open_access":"1"}],"arxiv":1,"conference":{"name":"POPL: Principles of Programming Languages","start_date":"2017-01-15","end_date":"2017-01-21","location":"Paris, France"},"date_published":"2017-01-01T00:00:00Z","alternative_title":["ACM SIGPLAN Notices"],"article_processing_charge":"No","publication_status":"published","year":"2017","quality_controlled":"1","intvolume":"        52","volume":52,"doi":"10.1145/3009837.3009873","isi":1,"external_id":{"isi":["000408311200013"],"arxiv":["1611.01063"]},"publisher":"ACM","department":[{"_id":"KrCh"}],"month":"01","day":"01","oa":1,"date_updated":"2026-04-07T13:27:56Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","related_material":{"record":[{"status":"public","relation":"dissertation_contains","id":"14539"}]},"page":"145 - 160","citation":{"mla":"Chatterjee, Krishnendu, et al. <i>Stochastic Invariants for Probabilistic Termination</i>. Vol. 52, no. 1, ACM, 2017, pp. 145–60, doi:<a href=\"https://doi.org/10.1145/3009837.3009873\">10.1145/3009837.3009873</a>.","ama":"Chatterjee K, Novotný P, Zikelic D. Stochastic invariants for probabilistic termination. In: Vol 52. ACM; 2017:145-160. doi:<a href=\"https://doi.org/10.1145/3009837.3009873\">10.1145/3009837.3009873</a>","ieee":"K. Chatterjee, P. Novotný, and D. Zikelic, “Stochastic invariants for probabilistic termination,” presented at the POPL: Principles of Programming Languages, Paris, France, 2017, vol. 52, no. 1, pp. 145–160.","ista":"Chatterjee K, Novotný P, Zikelic D. 2017. Stochastic invariants for probabilistic termination. POPL: Principles of Programming Languages, ACM SIGPLAN Notices, vol. 52, 145–160.","short":"K. Chatterjee, P. Novotný, D. Zikelic, in:, ACM, 2017, pp. 145–160.","chicago":"Chatterjee, Krishnendu, Petr Novotný, and Djordje Zikelic. “Stochastic Invariants for Probabilistic Termination,” 52:145–60. ACM, 2017. <a href=\"https://doi.org/10.1145/3009837.3009873\">https://doi.org/10.1145/3009837.3009873</a>.","apa":"Chatterjee, K., Novotný, P., &#38; Zikelic, D. (2017). Stochastic invariants for probabilistic termination (Vol. 52, pp. 145–160). Presented at the POPL: Principles of Programming Languages, Paris, France: ACM. <a href=\"https://doi.org/10.1145/3009837.3009873\">https://doi.org/10.1145/3009837.3009873</a>"},"project":[{"grant_number":"S 11407_N23","call_identifier":"FWF","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"grant_number":"S11402-N23","_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Moderne Concurrency Paradigms"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7"}],"oa_version":"Submitted Version","type":"conference","abstract":[{"lang":"eng","text":"Termination is one of the basic liveness properties, and we study the termination problem for probabilistic programs with real-valued variables. Previous works focused on the qualitative problem that asks whether an input program terminates with probability~1 (almost-sure termination). A powerful approach for this qualitative problem is the notion of ranking supermartingales with respect to a given set of invariants. The quantitative problem (probabilistic termination) asks for bounds on the termination probability. A fundamental and conceptual drawback of the existing approaches to address probabilistic termination is that even though the supermartingales consider the probabilistic behavior of the programs, the invariants are obtained completely ignoring the probabilistic aspect. In this work we address the probabilistic termination problem for linear-arithmetic probabilistic programs with nondeterminism. We define the notion of {\\em stochastic invariants}, which are constraints along with a probability bound that the constraints hold. We introduce a concept of {\\em repulsing supermartingales}. First, we show that repulsing supermartingales can be used to obtain bounds on the probability of the stochastic invariants. Second, we show the effectiveness of repulsing supermartingales in the following three ways: (1)~With a combination of ranking and repulsing supermartingales we can compute lower bounds on the probability of termination; (2)~repulsing supermartingales provide witnesses for refutation of almost-sure termination; and (3)~with a combination of ranking and repulsing supermartingales we can establish persistence properties of probabilistic programs. We also present results on related computational problems and an experimental evaluation of our approach on academic examples. "}],"title":"Stochastic invariants for probabilistic termination","_id":"1194","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Novotny, Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","first_name":"Petr","last_name":"Novotny"},{"first_name":"Djordje","last_name":"Zikelic","full_name":"Zikelic, Djordje"}],"status":"public","date_created":"2018-12-11T11:50:39Z","language":[{"iso":"eng"}],"publist_id":"6157","ec_funded":1,"publication_identifier":{"issn":["0730-8566"]},"scopus_import":"1","issue":"1"},{"abstract":[{"lang":"eng","text":"A standard objective in partially-observable Markov decision processes (POMDPs) is to find a policy that maximizes the expected discounted-sum payoff. However, such policies may still permit unlikely but highly undesirable outcomes, which is problematic especially in safety-critical applications. Recently, there has been a surge of interest in POMDPs where the goal is to maximize the probability to ensure that the payoff is at least a given threshold, but these approaches do not consider any optimization beyond satisfying this threshold constraint. In this work we go beyond both the “expectation” and “threshold” approaches and consider a “guaranteed payoff optimization (GPO)” problem for POMDPs, where we are given a threshold t and the objective is to find a policy σ such that a) each possible outcome of σ yields a discounted-sum payoff of at least t, and b) the expected discounted-sum payoff of σ is optimal (or near-optimal) among all policies satisfying a). We present a practical approach to tackle the GPO problem and evaluate it on standard POMDP benchmarks."}],"oa_version":"Submitted Version","type":"conference","status":"public","date_created":"2018-12-11T11:49:40Z","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee"},{"last_name":"Novotny","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotny, Petr"},{"last_name":"Pérez","first_name":"Guillermo","full_name":"Pérez, Guillermo"},{"first_name":"Jean","last_name":"Raskin","full_name":"Raskin, Jean"},{"full_name":"Zikelic, Djordje","first_name":"Djordje","last_name":"Zikelic"}],"_id":"1009","title":"Optimizing expectation with guarantees in POMDPs","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","date_updated":"2025-04-14T13:51:03Z","project":[{"grant_number":"S11407","_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory"},{"call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425"},{"grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification","_id":"25892FC0-B435-11E9-9278-68D0E5697425"}],"page":"3725 - 3732","citation":{"ieee":"K. Chatterjee, P. Novotný, G. Pérez, J. Raskin, and D. Zikelic, “Optimizing expectation with guarantees in POMDPs,” in <i>Proceedings of the 31st AAAI Conference on Artificial Intelligence</i>, San Francisco, CA, United States, 2017, vol. 5, pp. 3725–3732.","ista":"Chatterjee K, Novotný P, Pérez G, Raskin J, Zikelic D. 2017. Optimizing expectation with guarantees in POMDPs. Proceedings of the 31st AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 5, 3725–3732.","short":"K. Chatterjee, P. Novotný, G. Pérez, J. Raskin, D. Zikelic, in:, Proceedings of the 31st AAAI Conference on Artificial Intelligence, AAAI Press, 2017, pp. 3725–3732.","mla":"Chatterjee, Krishnendu, et al. “Optimizing Expectation with Guarantees in POMDPs.” <i>Proceedings of the 31st AAAI Conference on Artificial Intelligence</i>, vol. 5, AAAI Press, 2017, pp. 3725–32.","ama":"Chatterjee K, Novotný P, Pérez G, Raskin J, Zikelic D. Optimizing expectation with guarantees in POMDPs. In: <i>Proceedings of the 31st AAAI Conference on Artificial Intelligence</i>. Vol 5. AAAI Press; 2017:3725-3732.","apa":"Chatterjee, K., Novotný, P., Pérez, G., Raskin, J., &#38; Zikelic, D. (2017). Optimizing expectation with guarantees in POMDPs. In <i>Proceedings of the 31st AAAI Conference on Artificial Intelligence</i> (Vol. 5, pp. 3725–3732). San Francisco, CA, United States: AAAI Press.","chicago":"Chatterjee, Krishnendu, Petr Novotný, Guillermo Pérez, Jean Raskin, and Djordje Zikelic. “Optimizing Expectation with Guarantees in POMDPs.” In <i>Proceedings of the 31st AAAI Conference on Artificial Intelligence</i>, 5:3725–32. AAAI Press, 2017."},"acknowledgement":"he research leading to these results was supported by the Austrian Science Fund (FWF) NFN Grant no. S11407-N23 (RiSE/SHiNE); two ERC Starting grants (279307: Graph Games, 279499: inVEST); the Vienna Science and Tech- nology Fund (WWTF) through project ICT15-003; and the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007-2013) under REA grant agreement no. [291734].","ec_funded":1,"scopus_import":"1","publication":"Proceedings of the 31st AAAI Conference on Artificial Intelligence","publist_id":"6387","language":[{"iso":"eng"}],"intvolume":"         5","quality_controlled":"1","year":"2017","publication_status":"published","main_file_link":[{"url":"http://www.aaai.org/ocs/index.php/AAAI/AAAI17/paper/download/14354/14092","open_access":"1"}],"article_processing_charge":"No","date_published":"2017-01-01T00:00:00Z","conference":{"location":"San Francisco, CA, United States","name":"AAAI: Conference on Artificial Intelligence","start_date":"2017-02-04","end_date":"2017-02-10"},"month":"01","department":[{"_id":"KrCh"}],"publisher":"AAAI Press","external_id":{"isi":["000485630703107"]},"oa":1,"day":"01","volume":5,"isi":1},{"intvolume":"        59","year":"2016","quality_controlled":"1","publication_status":"published","ddc":["004"],"tmp":{"image":"/images/cc_by.png","legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"fulldoi":"https://doi.org/10.4230/LIPIcs.CONCUR.2016.10","alternative_title":["LIPIcs"],"date_published":"2016-08-01T00:00:00Z","file_date_updated":"2020-07-14T12:44:44Z","conference":{"location":"Quebec City, Canada","name":"CONCUR: Concurrency Theory","end_date":"2016-08-26","start_date":"2016-08-23"},"has_accepted_license":"1","month":"08","department":[{"_id":"KrCh"}],"publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","pubrep_id":"665","oa":1,"corr_author":"1","day":"01","file":[{"creator":"system","relation":"main_file","access_level":"open_access","checksum":"3c2dc6ab0358f8aa8f7aa7d6c1293159","date_created":"2018-12-12T10:16:40Z","file_size":553648,"file_name":"IST-2016-665-v1+1_Forejt_et_al__Stability_in_graphs_and_games.pdf","date_updated":"2020-07-14T12:44:44Z","content_type":"application/pdf","file_id":"5229"}],"doi":"10.4230/LIPIcs.CONCUR.2016.10","volume":59,"article_number":"10","abstract":[{"lang":"eng","text":"We study graphs and two-player games in which rewards are assigned to states, and the goal of the players is to satisfy or dissatisfy certain property of the generated outcome, given as a mean payoff property. Since the notion of mean-payoff does not reflect possible fluctuations from the mean-payoff along a run, we propose definitions and algorithms for capturing the stability of the system, and give algorithms for deciding if a given mean payoff and stability objective can be ensured in the system."}],"type":"conference","oa_version":"Published Version","author":[{"last_name":"Brázdil","first_name":"Tomáš","full_name":"Brázdil, Tomáš"},{"last_name":"Forejt","first_name":"Vojtěch","full_name":"Forejt, Vojtěch"},{"last_name":"Kučera","first_name":"Antonín","full_name":"Kučera, Antonín"},{"full_name":"Novotny, Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","first_name":"Petr","last_name":"Novotny"}],"status":"public","date_created":"2018-12-11T11:51:23Z","_id":"1325","title":"Stability in graphs and games","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","date_updated":"2024-10-09T20:57:03Z","project":[{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425"}],"citation":{"chicago":"Brázdil, Tomáš, Vojtěch Forejt, Antonín Kučera, and Petr Novotný. “Stability in Graphs and Games,” Vol. 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.10\">https://doi.org/10.4230/LIPIcs.CONCUR.2016.10</a>.","apa":"Brázdil, T., Forejt, V., Kučera, A., &#38; Novotný, P. (2016). Stability in graphs and games (Vol. 59). Presented at the CONCUR: Concurrency Theory, Quebec City, Canada: Schloss Dagstuhl - Leibniz-Zentrum für Informatik. <a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.10\">https://doi.org/10.4230/LIPIcs.CONCUR.2016.10</a>","mla":"Brázdil, Tomáš, et al. <i>Stability in Graphs and Games</i>. Vol. 59, 10, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.10\">10.4230/LIPIcs.CONCUR.2016.10</a>.","ama":"Brázdil T, Forejt V, Kučera A, Novotný P. Stability in graphs and games. In: Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:<a href=\"https://doi.org/10.4230/LIPIcs.CONCUR.2016.10\">10.4230/LIPIcs.CONCUR.2016.10</a>","ieee":"T. Brázdil, V. Forejt, A. Kučera, and P. Novotný, “Stability in graphs and games,” presented at the CONCUR: Concurrency Theory, Quebec City, Canada, 2016, vol. 59.","ista":"Brázdil T, Forejt V, Kučera A, Novotný P. 2016. Stability in graphs and games. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 10.","short":"T. Brázdil, V. Forejt, A. Kučera, P. Novotný, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016."},"acknowledgement":"The work has been supported by the Czech Science Foundation, grant No. 15-17564S, by EPSRC grant\r\nEP/M023656/1, and by the People Programme (Marie Curie Actions) of the European Union’s Seventh\r\nFramework Programme (FP7/2007-2013) under REA grant agreement no [291734]","ec_funded":1,"scopus_import":1,"language":[{"iso":"eng"}],"publist_id":"5944"},{"type":"conference","oa_version":"Preprint","abstract":[{"lang":"eng","text":"Energy Markov Decision Processes (EMDPs) are finite-state Markov decision processes where each transition is assigned an integer counter update and a rational payoff. An EMDP configuration is a pair s(n), where s is a control state and n is the current counter value. The configurations are changed by performing transitions in the standard way. We consider the problem of computing a safe strategy (i.e., a strategy that keeps the counter non-negative) which maximizes the expected mean payoff. "}],"title":"Optimizing the expected mean payoff in Energy Markov Decision Processes","_id":"1326","status":"public","author":[{"full_name":"Brázdil, Tomáš","first_name":"Tomáš","last_name":"Brázdil"},{"last_name":"Kučera","first_name":"Antonín","full_name":"Kučera, Antonín"},{"first_name":"Petr","last_name":"Novotny","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotny, Petr"}],"date_created":"2018-12-11T11:51:23Z","date_updated":"2025-09-22T08:25:26Z","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","citation":{"ama":"Brázdil T, Kučera A, Novotný P. Optimizing the expected mean payoff in Energy Markov Decision Processes. In: Vol 9938. Springer; 2016:32-49. doi:<a href=\"https://doi.org/10.1007/978-3-319-46520-3_3\">10.1007/978-3-319-46520-3_3</a>","mla":"Brázdil, Tomáš, et al. <i>Optimizing the Expected Mean Payoff in Energy Markov Decision Processes</i>. Vol. 9938, Springer, 2016, pp. 32–49, doi:<a href=\"https://doi.org/10.1007/978-3-319-46520-3_3\">10.1007/978-3-319-46520-3_3</a>.","ieee":"T. Brázdil, A. Kučera, and P. Novotný, “Optimizing the expected mean payoff in Energy Markov Decision Processes,” presented at the ATVA: Automated Technology for Verification and Analysis, Chiba, Japan, 2016, vol. 9938, pp. 32–49.","ista":"Brázdil T, Kučera A, Novotný P. 2016. Optimizing the expected mean payoff in Energy Markov Decision Processes. ATVA: Automated Technology for Verification and Analysis, LNCS, vol. 9938, 32–49.","short":"T. Brázdil, A. Kučera, P. Novotný, in:, Springer, 2016, pp. 32–49.","chicago":"Brázdil, Tomáš, Antonín Kučera, and Petr Novotný. “Optimizing the Expected Mean Payoff in Energy Markov Decision Processes,” 9938:32–49. Springer, 2016. <a href=\"https://doi.org/10.1007/978-3-319-46520-3_3\">https://doi.org/10.1007/978-3-319-46520-3_3</a>.","apa":"Brázdil, T., Kučera, A., &#38; Novotný, P. (2016). Optimizing the expected mean payoff in Energy Markov Decision Processes (Vol. 9938, pp. 32–49). Presented at the ATVA: Automated Technology for Verification and Analysis, Chiba, Japan: Springer. <a href=\"https://doi.org/10.1007/978-3-319-46520-3_3\">https://doi.org/10.1007/978-3-319-46520-3_3</a>"},"page":"32 - 49","project":[{"grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7"}],"ec_funded":1,"acknowledgement":"The research was funded by the Czech Science Foundation Grant No. P202/12/G061 and by the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007-2013) under REA grant agreement no [291734].","scopus_import":"1","language":[{"iso":"eng"}],"publist_id":"5943","publication_status":"published","year":"2016","quality_controlled":"1","intvolume":"      9938","fulldoi":"https://doi.org/10.1007/978-3-319-46520-3_3","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1607.00678"}],"arxiv":1,"conference":{"name":"ATVA: Automated Technology for Verification and Analysis","end_date":"2016-10-20","start_date":"2016-10-17","location":"Chiba, Japan"},"date_published":"2016-09-22T00:00:00Z","alternative_title":["LNCS"],"article_processing_charge":"No","external_id":{"arxiv":["1607.00678"],"isi":["000389808100003"]},"publisher":"Springer","month":"09","department":[{"_id":"KrCh"}],"day":"22","corr_author":"1","oa":1,"volume":9938,"doi":"10.1007/978-3-319-46520-3_3","isi":1},{"publication":"Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems","scopus_import":"1","ec_funded":1,"language":[{"iso":"eng"}],"publist_id":"5942","title":"Stochastic shortest path with energy constraints in POMDPs","_id":"1327","status":"public","author":[{"full_name":"Brázdil, Tomáš","last_name":"Brázdil","first_name":"Tomáš"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","first_name":"Martin","full_name":"Chmelik, Martin"},{"first_name":"Anchit","last_name":"Gupta","full_name":"Gupta, Anchit"},{"full_name":"Novotny, Petr","first_name":"Petr","last_name":"Novotny","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"}],"date_created":"2018-12-11T11:51:23Z","type":"conference","oa_version":"Preprint","abstract":[{"text":"We consider partially observable Markov decision processes (POMDPs) with a set of target states and positive integer costs associated with every transition. The traditional optimization objective (stochastic shortest path) asks to minimize the expected total cost until the target set is reached. We extend the traditional framework of POMDPs to model energy consumption, which represents a hard constraint. The energy levels may increase and decrease with transitions, and the hard constraint requires that the energy level must remain positive in all steps till the target is reached. First, we present a novel algorithm for solving POMDPs with energy levels, developing on existing POMDP solvers and using RTDP as its main method. Our second contribution is related to policy representation. For larger POMDP instances the policies computed by existing solvers are too large to be understandable. We present an automated procedure based on machine learning techniques that automatically extracts important decisions of the policy allowing us to compute succinct human readable policies. Finally, we show experimentally that our algorithm performs well and computes succinct policies on a number of POMDP instances from the literature that were naturally enhanced with energy levels. ","lang":"eng"}],"page":"1465 - 1466","citation":{"mla":"Brázdil, Tomáš, et al. “Stochastic Shortest Path with Energy Constraints in POMDPs.” <i>Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems</i>, ACM, 2016, pp. 1465–66.","ama":"Brázdil T, Chatterjee K, Chmelik M, Gupta A, Novotný P. Stochastic shortest path with energy constraints in POMDPs. In: <i>Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems</i>. ACM; 2016:1465-1466.","short":"T. Brázdil, K. Chatterjee, M. Chmelik, A. Gupta, P. Novotný, in:, Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems, ACM, 2016, pp. 1465–1466.","ista":"Brázdil T, Chatterjee K, Chmelik M, Gupta A, Novotný P. 2016. Stochastic shortest path with energy constraints in POMDPs. Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems. AAMAS: Autonomous Agents &#38; Multiagent Systems, 1465–1466.","ieee":"T. Brázdil, K. Chatterjee, M. Chmelik, A. Gupta, and P. Novotný, “Stochastic shortest path with energy constraints in POMDPs,” in <i>Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems</i>, Singapore, 2016, pp. 1465–1466.","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Anchit Gupta, and Petr Novotný. “Stochastic Shortest Path with Energy Constraints in POMDPs.” In <i>Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems</i>, 1465–66. ACM, 2016.","apa":"Brázdil, T., Chatterjee, K., Chmelik, M., Gupta, A., &#38; Novotný, P. (2016). Stochastic shortest path with energy constraints in POMDPs. In <i>Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems</i> (pp. 1465–1466). Singapore: ACM."},"project":[{"grant_number":"P 23499-N23","call_identifier":"FWF","name":"Modern Graph Algorithmic Techniques in Formal Verification","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"},{"_id":"25681D80-B435-11E9-9278-68D0E5697425","name":"International IST Postdoc Fellowship Programme","call_identifier":"FP7","grant_number":"291734"},{"grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7"}],"date_updated":"2025-06-04T10:26:23Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","day":"01","oa":1,"external_id":{"arxiv":["1602.07565"]},"publisher":"ACM","department":[{"_id":"KrCh"}],"month":"01","publication_status":"published","quality_controlled":"1","year":"2016","conference":{"name":"AAMAS: Autonomous Agents & Multiagent Systems","end_date":"2016-05-13","start_date":"2016-05-09","location":"Singapore"},"date_published":"2016-01-01T00:00:00Z","article_processing_charge":"No","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1602.07565"}],"arxiv":1},{"date_updated":"2025-04-15T08:12:22Z","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","page":"327 - 342","citation":{"mla":"Chatterjee, Krishnendu, et al. <i>Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs</i>. Vol. 20–22, ACM, 2016, pp. 327–42, doi:<a href=\"https://doi.org/10.1145/2837614.2837639\">10.1145/2837614.2837639</a>.","ama":"Chatterjee K, Fu H, Novotný P, Hasheminezhad R. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In: Vol 20-22. ACM; 2016:327-342. doi:<a href=\"https://doi.org/10.1145/2837614.2837639\">10.1145/2837614.2837639</a>","ieee":"K. Chatterjee, H. Fu, P. Novotný, and R. Hasheminezhad, “Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs,” presented at the POPL: Principles of Programming Languages, St. Petersburg, FL, USA, 2016, vol. 20–22, pp. 327–342.","short":"K. Chatterjee, H. Fu, P. Novotný, R. Hasheminezhad, in:, ACM, 2016, pp. 327–342.","ista":"Chatterjee K, Fu H, Novotný P, Hasheminezhad R. 2016. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. POPL: Principles of Programming Languages, POPL, vol. 20–22, 327–342.","chicago":"Chatterjee, Krishnendu, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad. “Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs,” 20–22:327–42. ACM, 2016. <a href=\"https://doi.org/10.1145/2837614.2837639\">https://doi.org/10.1145/2837614.2837639</a>.","apa":"Chatterjee, K., Fu, H., Novotný, P., &#38; Hasheminezhad, R. (2016). Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs (Vol. 20–22, pp. 327–342). Presented at the POPL: Principles of Programming Languages, St. Petersburg, FL, USA: ACM. <a href=\"https://doi.org/10.1145/2837614.2837639\">https://doi.org/10.1145/2837614.2837639</a>"},"project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","grant_number":"P 23499-N23"},{"name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23"},{"name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307"},{"grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"International IST Postdoc Fellowship Programme"}],"related_material":{"record":[{"id":"5993","relation":"later_version","status":"public"}]},"abstract":[{"lang":"eng","text":"In this paper, we consider termination of probabilistic programs with real-valued variables. The questions concerned are: (a) qualitative ones that ask (i) whether the program terminates with probability 1 (almost-sure termination) and (ii) whether the expected termination time is finite (finite termination); (b) quantitative ones that ask (i) to approximate the expected termination time (expectation problem) and (ii) to compute a bound B such that the probability to terminate after B steps decreases exponentially (concentration problem). To solve these questions, we utilize the notion of ranking supermartingales which is a powerful approach for proving termination of probabilistic programs. In detail, we focus on algorithmic synthesis of linear ranking-supermartingales over affine probabilistic programs (APP's) with both angelic and demonic non-determinism. An important subclass of APP's is LRAPP which is defined as the class of all APP's over which a linear ranking-supermartingale exists. Our main contributions are as follows. Firstly, we show that the membership problem of LRAPP (i) can be decided in polynomial time for APP's with at most demonic non-determinism, and (ii) is NP-hard and in PSPACE for APP's with angelic non-determinism; moreover, the NP-hardness result holds already for APP's without probability and demonic non-determinism. Secondly, we show that the concentration problem over LRAPP can be solved in the same complexity as for the membership problem of LRAPP. Finally, we show that the expectation problem over LRAPP can be solved in 2EXPTIME and is PSPACE-hard even for APP's without probability and non-determinism (i.e., deterministic programs). Our experimental results demonstrate the effectiveness of our approach to answer the qualitative and quantitative questions over APP's with at most demonic non-determinism."}],"type":"conference","oa_version":"Preprint","author":[{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"full_name":"Fu, Hongfei","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","first_name":"Hongfei","last_name":"Fu"},{"id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","last_name":"Novotny","first_name":"Petr","full_name":"Novotny, Petr"},{"last_name":"Hasheminezhad","first_name":"Rouzbeh","full_name":"Hasheminezhad, Rouzbeh"}],"date_created":"2018-12-11T11:52:01Z","status":"public","title":"Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs","_id":"1438","language":[{"iso":"eng"}],"publist_id":"5760","acknowledgement":"Supported by the Natural Science Foundation of China (NSFC) under Grant No. 61532019 ","ec_funded":1,"scopus_import":1,"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1510.08517"}],"arxiv":1,"fulldoi":"https://doi.org/10.1145/2837614.2837639","conference":{"start_date":"2016-01-20","end_date":"2016-01-22","name":"POPL: Principles of Programming Languages","location":"St. Petersburg, FL, USA"},"alternative_title":["POPL"],"date_published":"2016-01-11T00:00:00Z","publication_status":"published","quality_controlled":"1","year":"2016","doi":"10.1145/2837614.2837639","volume":"20-22","publisher":"ACM","month":"01","department":[{"_id":"KrCh"}],"external_id":{"arxiv":["1510.08517"]},"oa":1,"day":"11"}]