[{"date_updated":"2024-01-17T08:19:41Z","ddc":["000"],"file_date_updated":"2024-01-16T08:11:24Z","department":[{"_id":"KrCh"}],"_id":"14778","type":"journal_article","article_type":"original","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"status":"public","keyword":["Theoretical Computer Science","Software"],"publication_identifier":{"eissn":["1433-299X"],"issn":["0934-5043"]},"publication_status":"published","file":[{"creator":"dernst","date_updated":"2024-01-16T08:11:24Z","file_size":502522,"date_created":"2024-01-16T08:11:24Z","file_name":"2023_FormalAspectsComputing_Chatterjee.pdf","access_level":"open_access","relation":"main_file","content_type":"application/pdf","file_id":"14804","checksum":"3bb133eeb27ec01649a9a36445d952d9","success":1}],"language":[{"iso":"eng"}],"volume":35,"issue":"2","related_material":{"record":[{"status":"public","id":"10414","relation":"earlier_version"}]},"ec_funded":1,"license":"https://creativecommons.org/licenses/by/4.0/","abstract":[{"lang":"eng","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."}],"oa_version":"Published Version","month":"06","intvolume":" 35","citation":{"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.","chicago":"Chatterjee, Krishnendu, Ehsan Kafshdar Goharshady, Petr Novotný, Jiří Zárevúcky, and Dorde Zikelic. “On Lexicographic Proof Rules for Probabilistic Termination.” Formal Aspects of Computing. Association for Computing Machinery, 2023. https://doi.org/10.1145/3585391.","ieee":"K. Chatterjee, E. Kafshdar Goharshady, P. Novotný, J. Zárevúcky, and D. Zikelic, “On lexicographic proof rules for probabilistic termination,” Formal Aspects of Computing, vol. 35, no. 2. Association for Computing Machinery, 2023.","short":"K. Chatterjee, E. Kafshdar Goharshady, P. Novotný, J. Zárevúcky, D. Zikelic, Formal Aspects of Computing 35 (2023).","apa":"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. Association for Computing Machinery. https://doi.org/10.1145/3585391","ama":"Chatterjee K, Kafshdar Goharshady E, Novotný P, Zárevúcky J, Zikelic D. On lexicographic proof rules for probabilistic termination. Formal Aspects of Computing. 2023;35(2). doi:10.1145/3585391","mla":"Chatterjee, Krishnendu, et al. “On Lexicographic Proof Rules for Probabilistic Termination.” Formal Aspects of Computing, vol. 35, no. 2, 11, Association for Computing Machinery, 2023, doi:10.1145/3585391."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","author":[{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"last_name":"Kafshdar Goharshady","full_name":"Kafshdar Goharshady, Ehsan","first_name":"Ehsan"},{"first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotný, Petr","last_name":"Novotný"},{"first_name":"Jiří","full_name":"Zárevúcky, Jiří","last_name":"Zárevúcky"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","last_name":"Zikelic"}],"external_id":{"arxiv":["2108.02188"]},"article_processing_charge":"Yes (via OA deal)","title":"On lexicographic proof rules for probabilistic termination","article_number":"11","project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications"},{"name":"International IST Doctoral Program","grant_number":"665385","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"}],"has_accepted_license":"1","year":"2023","day":"23","publication":"Formal Aspects of Computing","date_published":"2023-06-23T00:00:00Z","doi":"10.1145/3585391","date_created":"2024-01-10T09:27:43Z","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.","quality_controlled":"1","publisher":"Association for Computing Machinery","oa":1},{"status":"public","type":"conference","conference":{"end_date":"2021-06-26","location":"Online","start_date":"2021-06-20","name":"PLDI: Programming Language Design and Implementation"},"_id":"9644","department":[{"_id":"KrCh"}],"date_updated":"2023-11-30T10:55:37Z","month":"06","scopus_import":"1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2104.01189"}],"oa_version":"Preprint","abstract":[{"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.","lang":"eng"}],"related_material":{"record":[{"id":"14539","status":"public","relation":"dissertation_contains"}]},"ec_funded":1,"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["9781450383912"]},"publication_status":"published","project":[{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"}],"title":"Proving non-termination by program reversal","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee"},{"first_name":"Ehsan Kafshdar","full_name":"Goharshady, Ehsan Kafshdar","last_name":"Goharshady"},{"full_name":"Novotný, Petr","last_name":"Novotný","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","first_name":"Petr"},{"orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","last_name":"Zikelic","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde"}],"article_processing_charge":"No","external_id":{"isi":["000723661700067"],"arxiv":["2104.01189"]},"user_id":"4359f0d1-fa6c-11eb-b949-802e58b17ae8","citation":{"mla":"Chatterjee, Krishnendu, et al. “Proving Non-Termination by Program Reversal.” Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Association for Computing Machinery, 2021, pp. 1033–48, doi:10.1145/3453483.3454093.","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.","ieee":"K. Chatterjee, E. K. Goharshady, P. Novotný, and D. Zikelic, “Proving non-termination by program reversal,” in Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Online, 2021, pp. 1033–1048.","apa":"Chatterjee, K., Goharshady, E. K., Novotný, P., & Zikelic, D. (2021). Proving non-termination by program reversal. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (pp. 1033–1048). Online: Association for Computing Machinery. https://doi.org/10.1145/3453483.3454093","ama":"Chatterjee K, Goharshady EK, Novotný P, Zikelic D. Proving non-termination by program reversal. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. Association for Computing Machinery; 2021:1033-1048. doi:10.1145/3453483.3454093","chicago":"Chatterjee, Krishnendu, Ehsan Kafshdar Goharshady, Petr Novotný, and Dorde Zikelic. “Proving Non-Termination by Program Reversal.” In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 1033–48. Association for Computing Machinery, 2021. https://doi.org/10.1145/3453483.3454093.","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."},"publisher":"Association for Computing Machinery","quality_controlled":"1","oa":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.","doi":"10.1145/3453483.3454093","date_published":"2021-06-01T00:00:00Z","date_created":"2021-07-11T22:01:17Z","page":"1033-1048","day":"01","publication":"Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation","isi":1,"year":"2021"},{"project":[{"call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","name":"Formal Methods for Stochastic Models: Algorithms and Applications","grant_number":"863818"},{"name":"International IST Doctoral Program","grant_number":"665385","call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"ieee":"K. Chatterjee, E. K. Goharshady, P. Novotný, J. Zárevúcky, and D. Zikelic, “On lexicographic proof rules for probabilistic termination,” in 24th International Symposium on Formal Methods, Virtual, 2021, vol. 13047, pp. 619–639.","short":"K. Chatterjee, E.K. Goharshady, P. Novotný, J. Zárevúcky, D. Zikelic, in:, 24th International Symposium on Formal Methods, Springer Nature, 2021, pp. 619–639.","ama":"Chatterjee K, Goharshady EK, Novotný P, Zárevúcky J, Zikelic D. On lexicographic proof rules for probabilistic termination. In: 24th International Symposium on Formal Methods. Vol 13047. Springer Nature; 2021:619-639. doi:10.1007/978-3-030-90870-6_33","apa":"Chatterjee, K., Goharshady, E. K., Novotný, P., Zárevúcky, J., & Zikelic, D. (2021). On lexicographic proof rules for probabilistic termination. In 24th International Symposium on Formal Methods (Vol. 13047, pp. 619–639). Virtual: Springer Nature. https://doi.org/10.1007/978-3-030-90870-6_33","mla":"Chatterjee, Krishnendu, et al. “On Lexicographic Proof Rules for Probabilistic Termination.” 24th International Symposium on Formal Methods, vol. 13047, Springer Nature, 2021, pp. 619–39, doi:10.1007/978-3-030-90870-6_33.","ista":"Chatterjee K, Goharshady EK, 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.","chicago":"Chatterjee, Krishnendu, Ehsan Kafshdar Goharshady, Petr Novotný, Jiří Zárevúcky, and Dorde Zikelic. “On Lexicographic Proof Rules for Probabilistic Termination.” In 24th International Symposium on Formal Methods, 13047:619–39. Springer Nature, 2021. https://doi.org/10.1007/978-3-030-90870-6_33."},"title":"On lexicographic proof rules for probabilistic termination","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"first_name":"Ehsan Kafshdar","last_name":"Goharshady","full_name":"Goharshady, Ehsan Kafshdar"},{"last_name":"Novotný","full_name":"Novotný, Petr","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Zárevúcky, Jiří","last_name":"Zárevúcky","first_name":"Jiří"},{"last_name":"Zikelic","full_name":"Zikelic, Dorde","orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde"}],"external_id":{"arxiv":["2108.02188"],"isi":["000758218600033"]},"article_processing_charge":"No","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.","quality_controlled":"1","publisher":"Springer Nature","oa":1,"day":"10","publication":"24th International Symposium on Formal Methods","isi":1,"year":"2021","doi":"10.1007/978-3-030-90870-6_33","date_published":"2021-11-10T00:00:00Z","date_created":"2021-12-05T23:01:45Z","page":"619-639","_id":"10414","status":"public","type":"conference","conference":{"name":"FM: Formal Methods","location":"Virtual","end_date":"2021-11-26","start_date":"2021-11-20"},"date_updated":"2024-01-17T08:19:41Z","department":[{"_id":"KrCh"}],"oa_version":"Preprint","abstract":[{"lang":"eng","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."}],"month":"11","intvolume":" 13047","alternative_title":["LNCS"],"scopus_import":"1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2108.02188"}],"language":[{"iso":"eng"}],"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9-783-0309-0869-0"],"eisbn":["978-3-030-90870-6"]},"publication_status":"published","volume":13047,"related_material":{"record":[{"id":"14539","status":"public","relation":"dissertation_contains"},{"relation":"later_version","id":"14778","status":"public"}]},"ec_funded":1},{"publisher":"Association for the Advancement of Artificial Intelligence","quality_controlled":"1","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.","page":"48-56","date_published":"2020-06-01T00:00:00Z","date_created":"2020-08-02T22:00:58Z","year":"2020","day":"01","publication":"Proceedings of the 30th International Conference on Automated Planning and Scheduling","project":[{"call_identifier":"FWF","_id":"25863FF4-B435-11E9-9278-68D0E5697425","grant_number":"S11407","name":"Game Theory"}],"author":[{"last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu"},{"first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","last_name":"Chmelik","full_name":"Chmelik, Martin"},{"first_name":"Deep","full_name":"Karkhanis, Deep","last_name":"Karkhanis"},{"full_name":"Novotný, Petr","last_name":"Novotný","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0002-8407-0705","full_name":"Royer, Amélie","last_name":"Royer","id":"3811D890-F248-11E8-B48F-1D18A9856A87","first_name":"Amélie"}],"article_processing_charge":"No","title":"Multiple-environment Markov decision processes: Efficient analysis and applications","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.","chicago":"Chatterjee, Krishnendu, Martin Chmelik, Deep Karkhanis, Petr Novotný, and Amélie Royer. “Multiple-Environment Markov Decision Processes: Efficient Analysis and Applications.” In Proceedings of the 30th International Conference on Automated Planning and Scheduling, 30:48–56. Association for the Advancement of Artificial Intelligence, 2020.","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 Proceedings of the 30th International Conference on Automated Planning and Scheduling, Nancy, France, 2020, vol. 30, pp. 48–56.","apa":"Chatterjee, K., Chmelik, M., Karkhanis, D., Novotný, P., & Royer, A. (2020). Multiple-environment Markov decision processes: Efficient analysis and applications. In Proceedings of the 30th International Conference on Automated Planning and Scheduling (Vol. 30, pp. 48–56). Nancy, France: Association for the Advancement of Artificial Intelligence.","ama":"Chatterjee K, Chmelik M, Karkhanis D, Novotný P, Royer A. Multiple-environment Markov decision processes: Efficient analysis and applications. In: Proceedings of the 30th International Conference on Automated Planning and Scheduling. Vol 30. Association for the Advancement of Artificial Intelligence; 2020:48-56.","mla":"Chatterjee, Krishnendu, et al. “Multiple-Environment Markov Decision Processes: Efficient Analysis and Applications.” Proceedings of the 30th International Conference on Automated Planning and Scheduling, vol. 30, Association for the Advancement of Artificial Intelligence, 2020, pp. 48–56."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","scopus_import":"1","month":"06","intvolume":" 30","abstract":[{"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.","lang":"eng"}],"oa_version":"None","volume":30,"related_material":{"record":[{"status":"public","id":"8390","relation":"dissertation_contains"}]},"publication_identifier":{"eissn":["23340843"],"issn":["23340835"]},"publication_status":"published","language":[{"iso":"eng"}],"type":"conference","conference":{"name":"ICAPS: International Conference on Automated Planning and Scheduling","start_date":"2020-10-26","end_date":"2020-10-30","location":"Nancy, France"},"status":"public","_id":"8193","department":[{"_id":"KrCh"}],"date_updated":"2023-09-07T13:16:18Z"},{"volume":11781,"language":[{"iso":"eng"}],"publication_status":"published","publication_identifier":{"isbn":["9783030317836"],"eissn":["16113349"],"issn":["03029743"]},"intvolume":" 11781","month":"10","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1907.11010"}],"scopus_import":"1","alternative_title":["LNCS"],"oa_version":"Preprint","abstract":[{"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).","lang":"eng"}],"department":[{"_id":"KrCh"}],"date_updated":"2023-09-06T12:40:58Z","status":"public","conference":{"name":"ATVA: Automated TEchnology for Verification and Analysis","start_date":"2019-10-28","location":"Taipei, Taiwan","end_date":"2019-10-31"},"type":"conference","_id":"7183","date_created":"2019-12-15T23:00:44Z","date_published":"2019-10-21T00:00:00Z","doi":"10.1007/978-3-030-31784-3_27","page":"462-478","publication":"International Symposium on Automated Technology for Verification and Analysis","day":"21","year":"2019","isi":1,"oa":1,"quality_controlled":"1","publisher":"Springer Nature","title":"Deciding fast termination for probabilistic VASS with nondeterminism","external_id":{"arxiv":["1907.11010"],"isi":["000723515700027"]},"article_processing_charge":"No","author":[{"last_name":"Brázdil","full_name":"Brázdil, Tomás","first_name":"Tomás"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"full_name":"Kucera, Antonín","last_name":"Kucera","first_name":"Antonín"},{"first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","last_name":"Novotný","full_name":"Novotný, Petr"},{"full_name":"Velan, Dominik","last_name":"Velan","first_name":"Dominik"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"ieee":"T. Brázdil, K. Chatterjee, A. Kucera, P. Novotný, and D. Velan, “Deciding fast termination for probabilistic VASS with nondeterminism,” in International Symposium on Automated Technology for Verification and Analysis, Taipei, Taiwan, 2019, vol. 11781, pp. 462–478.","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.","apa":"Brázdil, T., Chatterjee, K., Kucera, A., Novotný, P., & Velan, D. (2019). Deciding fast termination for probabilistic VASS with nondeterminism. In International Symposium on Automated Technology for Verification and Analysis (Vol. 11781, pp. 462–478). Taipei, Taiwan: Springer Nature. https://doi.org/10.1007/978-3-030-31784-3_27","ama":"Brázdil T, Chatterjee K, Kucera A, Novotný P, Velan D. Deciding fast termination for probabilistic VASS with nondeterminism. In: International Symposium on Automated Technology for Verification and Analysis. Vol 11781. Springer Nature; 2019:462-478. doi:10.1007/978-3-030-31784-3_27","mla":"Brázdil, Tomás, et al. “Deciding Fast Termination for Probabilistic VASS with Nondeterminism.” International Symposium on Automated Technology for Verification and Analysis, vol. 11781, Springer Nature, 2019, pp. 462–78, doi:10.1007/978-3-030-31784-3_27.","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.","chicago":"Brázdil, Tomás, Krishnendu Chatterjee, Antonín Kucera, Petr Novotný, and Dominik Velan. “Deciding Fast Termination for Probabilistic VASS with Nondeterminism.” In International Symposium on Automated Technology for Verification and Analysis, 11781:462–78. Springer Nature, 2019. https://doi.org/10.1007/978-3-030-31784-3_27."},"project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}]},{"date_updated":"2021-01-12T07:42:07Z","department":[{"_id":"KrCh"}],"_id":"325","status":"public","type":"conference","conference":{"start_date":"2018-01-07","location":"Los Angeles, CA, USA","end_date":"2018-01-13","name":"POPL: Principles of Programming Languages"},"language":[{"iso":"eng"}],"publication_status":"published","issue":"POPL","volume":2,"oa_version":"Preprint","abstract":[{"lang":"eng","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."}],"month":"01","intvolume":" 2","main_file_link":[{"url":"https://arxiv.org/abs/1709.04037","open_access":"1"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","citation":{"chicago":"Agrawal, Sheshansh, Krishnendu Chatterjee, and Petr Novotný. “Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs,” Vol. 2. ACM, 2018. https://doi.org/10.1145/3158122.","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.","mla":"Agrawal, Sheshansh, et al. Lexicographic Ranking Supermartingales: An Efficient Approach to Termination of Probabilistic Programs. Vol. 2, no. POPL, 34, ACM, 2018, doi:10.1145/3158122.","apa":"Agrawal, S., Chatterjee, K., & 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. https://doi.org/10.1145/3158122","ama":"Agrawal S, Chatterjee K, Novotný P. Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. In: Vol 2. ACM; 2018. doi:10.1145/3158122","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.","short":"S. Agrawal, K. Chatterjee, P. Novotný, in:, ACM, 2018."},"title":"Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs","author":[{"full_name":"Agrawal, Sheshansh","last_name":"Agrawal","first_name":"Sheshansh"},{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Novotny","full_name":"Novotny, Petr","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"7540","external_id":{"arxiv":["1709.04037"]},"article_number":"34","project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"}],"day":"01","year":"2018","doi":"10.1145/3158122","date_published":"2018-01-01T00:00:00Z","date_created":"2018-12-11T11:45:50Z","quality_controlled":"1","publisher":"ACM","oa":1},{"quality_controlled":"1","publisher":"IEEE","oa":1,"date_published":"2018-07-09T00:00:00Z","doi":"10.1145/3209108.3209191","date_created":"2018-12-11T11:44:51Z","page":"185 - 194","day":"09","isi":1,"year":"2018","project":[{"name":"Efficient Algorithms for Computer Aided Verification","grant_number":"ICT15-003","_id":"25892FC0-B435-11E9-9278-68D0E5697425"},{"_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","name":"Rigorous Systems Engineering","grant_number":"S 11407_N23"}],"title":"Efficient algorithms for asymptotic bounds on termination time in VASS","publist_id":"7780","author":[{"last_name":"Brázdil","full_name":"Brázdil, Tomáš","first_name":"Tomáš"},{"orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Antonín","full_name":"Kučera, Antonín","last_name":"Kučera"},{"id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","first_name":"Petr","full_name":"Novotny, Petr","last_name":"Novotny"},{"first_name":"Dominik","last_name":"Velan","full_name":"Velan, Dominik"},{"last_name":"Zuleger","full_name":"Zuleger, Florian","first_name":"Florian"}],"external_id":{"isi":["000545262800020"]},"article_processing_charge":"No","user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"apa":"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 (Vol. F138033, pp. 185–194). Presented at the LICS: Logic in Computer Science, Oxford, United Kingdom: IEEE. https://doi.org/10.1145/3209108.3209191","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:10.1145/3209108.3209191","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.","mla":"Brázdil, Tomáš, et al. Efficient Algorithms for Asymptotic Bounds on Termination Time in VASS. Vol. F138033, IEEE, 2018, pp. 185–94, doi:10.1145/3209108.3209191.","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.","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. https://doi.org/10.1145/3209108.3209191."},"month":"07","scopus_import":"1","alternative_title":["ACM/IEEE Symposium on Logic in Computer Science"],"main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1804.10985"}],"oa_version":"Preprint","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."}],"volume":"F138033","ec_funded":1,"language":[{"iso":"eng"}],"publication_identifier":{"isbn":["978-1-4503-5583-4"]},"publication_status":"published","status":"public","type":"conference","conference":{"name":"LICS: Logic in Computer Science","end_date":"2018-07-12","location":"Oxford, United Kingdom","start_date":"2018-07-09"},"_id":"143","department":[{"_id":"KrCh"}],"date_updated":"2023-09-11T13:23:42Z"},{"department":[{"_id":"KrCh"}],"date_updated":"2023-09-19T14:38:42Z","type":"journal_article","status":"public","_id":"5993","volume":40,"related_material":{"record":[{"id":"1438","status":"public","relation":"earlier_version"}]},"issue":"2","ec_funded":1,"publication_identifier":{"issn":["0164-0925"]},"publication_status":"published","language":[{"iso":"eng"}],"scopus_import":"1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1510.08517"}],"month":"06","intvolume":" 40","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"}],"oa_version":"Submitted Version","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee"},{"first_name":"Hongfei","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","full_name":"Fu, Hongfei","last_name":"Fu"},{"last_name":"Novotný","full_name":"Novotný, Petr","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Rouzbeh","full_name":"Hasheminezhad, Rouzbeh","last_name":"Hasheminezhad"}],"article_processing_charge":"No","external_id":{"isi":["000434634500003"],"arxiv":["1510.08517"]},"title":"Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs","citation":{"ama":"Chatterjee K, Fu H, Novotný P, Hasheminezhad R. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. ACM Transactions on Programming Languages and Systems. 2018;40(2). doi:10.1145/3174800","apa":"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. Association for Computing Machinery (ACM). https://doi.org/10.1145/3174800","short":"K. Chatterjee, H. Fu, P. Novotný, R. Hasheminezhad, ACM Transactions on Programming Languages and Systems 40 (2018).","ieee":"K. Chatterjee, H. Fu, P. Novotný, and R. Hasheminezhad, “Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs,” ACM Transactions on Programming Languages and Systems, vol. 40, no. 2. Association for Computing Machinery (ACM), 2018.","mla":"Chatterjee, Krishnendu, et al. “Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs.” ACM Transactions on Programming Languages and Systems, vol. 40, no. 2, 7, Association for Computing Machinery (ACM), 2018, doi:10.1145/3174800.","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.","chicago":"Chatterjee, Krishnendu, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad. “Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs.” ACM Transactions on Programming Languages and Systems. Association for Computing Machinery (ACM), 2018. https://doi.org/10.1145/3174800."},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","project":[{"_id":"2584A770-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification"},{"name":"Rigorous Systems Engineering","grant_number":"S 11407_N23","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425","grant_number":"291734","name":"International IST Postdoc Fellowship Programme"}],"article_number":"7","date_published":"2018-06-01T00:00:00Z","doi":"10.1145/3174800","date_created":"2019-02-14T12:29:10Z","isi":1,"year":"2018","day":"01","publication":"ACM Transactions on Programming Languages and Systems","quality_controlled":"1","publisher":"Association for Computing Machinery (ACM)","oa":1},{"status":"public","conference":{"name":"IJCAI: International Joint Conference on Artificial Intelligence","end_date":"2018-07-19","location":"Stockholm, Sweden","start_date":"2018-07-13"},"type":"conference","_id":"24","department":[{"_id":"KrCh"},{"_id":"ToHe"}],"date_updated":"2023-09-19T14:45:48Z","intvolume":" 2018","month":"07","main_file_link":[{"url":"https://arxiv.org/abs/1804.10601","open_access":"1"}],"scopus_import":"1","oa_version":"Preprint","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."}],"ec_funded":1,"volume":2018,"language":[{"iso":"eng"}],"publication_status":"published","project":[{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications"}],"title":"Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum objectives","external_id":{"isi":["000764175404117"],"arxiv":["1804.10601"]},"article_processing_charge":"No","publist_id":"8031","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Adrian","id":"4A2E9DBA-F248-11E8-B48F-1D18A9856A87","full_name":"Elgyütt, Adrian","last_name":"Elgyütt"},{"id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","first_name":"Petr","last_name":"Novotny","full_name":"Novotny, Petr"},{"last_name":"Rouillé","full_name":"Rouillé, Owen","first_name":"Owen"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","citation":{"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.","apa":"Chatterjee, K., Elgyütt, A., Novotný, P., & 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. https://doi.org/10.24963/ijcai.2018/652","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:10.24963/ijcai.2018/652","mla":"Chatterjee, Krishnendu, et al. Expectation Optimization with Probabilistic Guarantees in POMDPs with Discounted-Sum Objectives. Vol. 2018, IJCAI, 2018, pp. 4692–99, doi:10.24963/ijcai.2018/652.","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. https://doi.org/10.24963/ijcai.2018/652."},"oa":1,"quality_controlled":"1","publisher":"IJCAI","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","date_created":"2018-12-11T11:44:13Z","date_published":"2018-07-01T00:00:00Z","doi":"10.24963/ijcai.2018/652","page":"4692 - 4699","day":"01","year":"2018","isi":1},{"ec_funded":1,"volume":5,"publication_status":"published","language":[{"iso":"eng"}],"main_file_link":[{"url":"http://www.aaai.org/ocs/index.php/AAAI/AAAI17/paper/download/14354/14092","open_access":"1"}],"scopus_import":"1","intvolume":" 5","month":"01","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","department":[{"_id":"KrCh"}],"date_updated":"2023-09-22T09:46:41Z","conference":{"start_date":"2017-02-04","location":"San Francisco, CA, United States","end_date":"2017-02-10","name":"AAAI: Conference on Artificial Intelligence"},"type":"conference","status":"public","_id":"1009","page":"3725 - 3732","date_created":"2018-12-11T11:49:40Z","date_published":"2017-01-01T00:00:00Z","year":"2017","isi":1,"publication":"Proceedings of the 31st AAAI Conference on Artificial Intelligence","day":"01","oa":1,"quality_controlled":"1","publisher":"AAAI Press","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].","article_processing_charge":"No","external_id":{"isi":["000485630703107"]},"publist_id":"6387","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Novotny","full_name":"Novotny, Petr","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"},{"first_name":"Guillermo","last_name":"Pérez","full_name":"Pérez, Guillermo"},{"full_name":"Raskin, Jean","last_name":"Raskin","first_name":"Jean"},{"first_name":"Djordje","full_name":"Zikelic, Djordje","last_name":"Zikelic"}],"title":"Optimizing expectation with guarantees in POMDPs","citation":{"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.","ieee":"K. Chatterjee, P. Novotný, G. Pérez, J. Raskin, and D. Zikelic, “Optimizing expectation with guarantees in POMDPs,” in Proceedings of the 31st AAAI Conference on Artificial Intelligence, San Francisco, CA, United States, 2017, vol. 5, pp. 3725–3732.","ama":"Chatterjee K, Novotný P, Pérez G, Raskin J, Zikelic D. Optimizing expectation with guarantees in POMDPs. In: Proceedings of the 31st AAAI Conference on Artificial Intelligence. Vol 5. AAAI Press; 2017:3725-3732.","apa":"Chatterjee, K., Novotný, P., Pérez, G., Raskin, J., & Zikelic, D. (2017). Optimizing expectation with guarantees in POMDPs. In Proceedings of the 31st AAAI Conference on Artificial Intelligence (Vol. 5, pp. 3725–3732). San Francisco, CA, United States: AAAI Press.","mla":"Chatterjee, Krishnendu, et al. “Optimizing Expectation with Guarantees in POMDPs.” Proceedings of the 31st AAAI Conference on Artificial Intelligence, vol. 5, AAAI Press, 2017, pp. 3725–32.","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.","chicago":"Chatterjee, Krishnendu, Petr Novotný, Guillermo Pérez, Jean Raskin, and Djordje Zikelic. “Optimizing Expectation with Guarantees in POMDPs.” In Proceedings of the 31st AAAI Conference on Artificial Intelligence, 5:3725–32. AAAI Press, 2017."},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","project":[{"_id":"25863FF4-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"Game Theory","grant_number":"S11407"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"},{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","call_identifier":"FP7","_id":"25681D80-B435-11E9-9278-68D0E5697425"},{"_id":"25892FC0-B435-11E9-9278-68D0E5697425","grant_number":"ICT15-003","name":"Efficient Algorithms for Computer Aided Verification"}]},{"publisher":"ACM","quality_controlled":"1","oa":1,"isi":1,"year":"2017","day":"01","page":"145 - 160","doi":"10.1145/3009837.3009873","date_published":"2017-01-01T00:00:00Z","date_created":"2018-12-11T11:50:39Z","project":[{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"25F5A88A-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S11402-N23","name":"Moderne Concurrency Paradigms"},{"name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"citation":{"short":"K. Chatterjee, P. Novotný, D. Zikelic, in:, ACM, 2017, pp. 145–160.","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.","apa":"Chatterjee, K., Novotný, P., & Zikelic, D. (2017). Stochastic invariants for probabilistic termination (Vol. 52, pp. 145–160). Presented at the POPL: Principles of Programming Languages, Paris, France: ACM. https://doi.org/10.1145/3009837.3009873","ama":"Chatterjee K, Novotný P, Zikelic D. Stochastic invariants for probabilistic termination. In: Vol 52. ACM; 2017:145-160. doi:10.1145/3009837.3009873","mla":"Chatterjee, Krishnendu, et al. Stochastic Invariants for Probabilistic Termination. Vol. 52, no. 1, ACM, 2017, pp. 145–60, doi:10.1145/3009837.3009873.","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.","chicago":"Chatterjee, Krishnendu, Petr Novotný, and Djordje Zikelic. “Stochastic Invariants for Probabilistic Termination,” 52:145–60. ACM, 2017. https://doi.org/10.1145/3009837.3009873."},"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publist_id":"6157","author":[{"first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Novotny, Petr","last_name":"Novotny","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"},{"full_name":"Zikelic, Djordje","last_name":"Zikelic","first_name":"Djordje"}],"external_id":{"isi":["000408311200013"]},"article_processing_charge":"No","title":"Stochastic invariants for probabilistic termination","abstract":[{"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. ","lang":"eng"}],"oa_version":"Submitted Version","alternative_title":["ACM SIGPLAN Notices"],"scopus_import":"1","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1611.01063"}],"month":"01","intvolume":" 52","publication_identifier":{"issn":["07308566"]},"publication_status":"published","language":[{"iso":"eng"}],"volume":52,"related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"14539"}]},"issue":"1","ec_funded":1,"_id":"1194","type":"conference","conference":{"name":"POPL: Principles of Programming Languages","start_date":"2017-01-15","location":"Paris, France","end_date":"2017-01-21"},"status":"public","date_updated":"2023-11-30T10:55:36Z","department":[{"_id":"KrCh"}]},{"publication_status":"published","file":[{"file_name":"IST-2016-665-v1+1_Forejt_et_al__Stability_in_graphs_and_games.pdf","date_created":"2018-12-12T10:16:40Z","creator":"system","file_size":553648,"date_updated":"2020-07-14T12:44:44Z","file_id":"5229","checksum":"3c2dc6ab0358f8aa8f7aa7d6c1293159","relation":"main_file","access_level":"open_access","content_type":"application/pdf"}],"language":[{"iso":"eng"}],"volume":59,"ec_funded":1,"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."}],"oa_version":"Published Version","alternative_title":["LIPIcs"],"scopus_import":1,"month":"08","intvolume":" 59","date_updated":"2021-01-12T06:49:53Z","ddc":["004"],"department":[{"_id":"KrCh"}],"file_date_updated":"2020-07-14T12:44:44Z","_id":"1325","type":"conference","conference":{"name":"CONCUR: Concurrency Theory","location":"Quebec City, Canada","end_date":"2016-08-26","start_date":"2016-08-23"},"tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)","short":"CC BY (4.0)"},"status":"public","pubrep_id":"665","has_accepted_license":"1","year":"2016","day":"01","doi":"10.4230/LIPIcs.CONCUR.2016.10","date_published":"2016-08-01T00:00:00Z","date_created":"2018-12-11T11:51:23Z","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]","quality_controlled":"1","publisher":"Schloss Dagstuhl - Leibniz-Zentrum für Informatik","oa":1,"citation":{"apa":"Brázdil, T., Forejt, V., Kučera, A., & 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. https://doi.org/10.4230/LIPIcs.CONCUR.2016.10","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:10.4230/LIPIcs.CONCUR.2016.10","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.","short":"T. Brázdil, V. Forejt, A. Kučera, P. Novotný, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.","mla":"Brázdil, Tomáš, et al. Stability in Graphs and Games. Vol. 59, 10, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016, doi:10.4230/LIPIcs.CONCUR.2016.10.","ista":"Brázdil T, Forejt V, Kučera A, Novotný P. 2016. Stability in graphs and games. CONCUR: Concurrency Theory, LIPIcs, vol. 59, 10.","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. https://doi.org/10.4230/LIPIcs.CONCUR.2016.10."},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","author":[{"first_name":"Tomáš","last_name":"Brázdil","full_name":"Brázdil, Tomáš"},{"full_name":"Forejt, Vojtěch","last_name":"Forejt","first_name":"Vojtěch"},{"full_name":"Kučera, Antonín","last_name":"Kučera","first_name":"Antonín"},{"first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotny, Petr","last_name":"Novotny"}],"publist_id":"5944","title":"Stability in graphs and games","article_number":"10","project":[{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}]},{"department":[{"_id":"KrCh"}],"title":"Stochastic shortest path with energy constraints in POMDPs","author":[{"full_name":"Brázdil, Tomáš","last_name":"Brázdil","first_name":"Tomáš"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"first_name":"Martin","id":"3624234E-F248-11E8-B48F-1D18A9856A87","full_name":"Chmelik, Martin","last_name":"Chmelik"},{"last_name":"Gupta","full_name":"Gupta, Anchit","first_name":"Anchit"},{"first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","last_name":"Novotny","full_name":"Novotny, Petr"}],"publist_id":"5942","user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"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 & Multiagent Systems, 1465–1466.","chicago":"Brázdil, Tomáš, Krishnendu Chatterjee, Martin Chmelik, Anchit Gupta, and Petr Novotný. “Stochastic Shortest Path with Energy Constraints in POMDPs.” In Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems, 1465–66. ACM, 2016.","ieee":"T. Brázdil, K. Chatterjee, M. Chmelik, A. Gupta, and P. Novotný, “Stochastic shortest path with energy constraints in POMDPs,” in Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems, Singapore, 2016, pp. 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.","apa":"Brázdil, T., Chatterjee, K., Chmelik, M., Gupta, A., & Novotný, P. (2016). Stochastic shortest path with energy constraints in POMDPs. In Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems (pp. 1465–1466). Singapore: ACM.","ama":"Brázdil T, Chatterjee K, Chmelik M, Gupta A, Novotný P. Stochastic shortest path with energy constraints in POMDPs. In: Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems. ACM; 2016:1465-1466.","mla":"Brázdil, Tomáš, et al. “Stochastic Shortest Path with Energy Constraints in POMDPs.” Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems, ACM, 2016, pp. 1465–66."},"date_updated":"2021-01-12T06:49:54Z","status":"public","project":[{"grant_number":"P 23499-N23","name":"Modern Graph Algorithmic Techniques in Formal Verification","call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425"},{"_id":"25832EC2-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425"}],"conference":{"location":"Singapore","end_date":"2016-05-13","start_date":"2016-05-09","name":"AAMAS: Autonomous Agents & Multiagent Systems"},"type":"conference","_id":"1327","ec_funded":1,"date_created":"2018-12-11T11:51:23Z","date_published":"2016-01-01T00:00:00Z","page":"1465 - 1466","language":[{"iso":"eng"}],"publication":"Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems","day":"01","publication_status":"published","year":"2016","month":"01","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1602.07565"}],"oa":1,"publisher":"ACM","quality_controlled":"1","scopus_import":1,"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"}]},{"_id":"1326","status":"public","conference":{"name":"ATVA: Automated Technology for Verification and Analysis","location":"Chiba, Japan","end_date":"2016-10-20","start_date":"2016-10-17"},"type":"conference","date_updated":"2021-01-12T06:49:53Z","department":[{"_id":"KrCh"}],"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. "}],"intvolume":" 9938","month":"09","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/1607.00678"}],"alternative_title":["LNCS"],"scopus_import":1,"language":[{"iso":"eng"}],"publication_status":"published","ec_funded":1,"volume":9938,"project":[{"_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7","grant_number":"291734","name":"International IST Postdoc Fellowship Programme"}],"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","citation":{"apa":"Brázdil, T., Kučera, A., & 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. https://doi.org/10.1007/978-3-319-46520-3_3","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:10.1007/978-3-319-46520-3_3","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.","short":"T. Brázdil, A. Kučera, P. Novotný, in:, Springer, 2016, pp. 32–49.","mla":"Brázdil, Tomáš, et al. Optimizing the Expected Mean Payoff in Energy Markov Decision Processes. Vol. 9938, Springer, 2016, pp. 32–49, doi:10.1007/978-3-319-46520-3_3.","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.","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. https://doi.org/10.1007/978-3-319-46520-3_3."},"title":"Optimizing the expected mean payoff in Energy Markov Decision Processes","author":[{"first_name":"Tomáš","last_name":"Brázdil","full_name":"Brázdil, Tomáš"},{"first_name":"Antonín","last_name":"Kučera","full_name":"Kučera, Antonín"},{"last_name":"Novotny","full_name":"Novotny, Petr","first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87"}],"publist_id":"5943","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].","oa":1,"publisher":"Springer","quality_controlled":"1","day":"22","year":"2016","date_created":"2018-12-11T11:51:23Z","date_published":"2016-09-22T00:00:00Z","doi":"10.1007/978-3-319-46520-3_3","page":"32 - 49"},{"type":"conference","conference":{"name":"POPL: Principles of Programming Languages","start_date":"2016-01-20","location":"St. Petersburg, FL, USA","end_date":"2016-01-22"},"status":"public","_id":"1438","department":[{"_id":"KrCh"}],"date_updated":"2023-09-19T14:38:41Z","alternative_title":["POPL"],"scopus_import":1,"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1510.08517"}],"month":"01","abstract":[{"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.","lang":"eng"}],"oa_version":"Preprint","volume":"20-22","related_material":{"record":[{"id":"5993","status":"public","relation":"later_version"}]},"ec_funded":1,"publication_status":"published","language":[{"iso":"eng"}],"project":[{"call_identifier":"FWF","_id":"2584A770-B435-11E9-9278-68D0E5697425","name":"Modern Graph Algorithmic Techniques in Formal Verification","grant_number":"P 23499-N23"},{"call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425","grant_number":"S 11407_N23","name":"Rigorous Systems Engineering"},{"call_identifier":"FP7","_id":"2581B60A-B435-11E9-9278-68D0E5697425","name":"Quantitative Graph Games: Theory and Applications","grant_number":"279307"},{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"},{"full_name":"Fu, Hongfei","last_name":"Fu","id":"3AAD03D6-F248-11E8-B48F-1D18A9856A87","first_name":"Hongfei"},{"full_name":"Novotny, Petr","last_name":"Novotny","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","first_name":"Petr"},{"last_name":"Hasheminezhad","full_name":"Hasheminezhad, Rouzbeh","first_name":"Rouzbeh"}],"publist_id":"5760","external_id":{"arxiv":["1510.08517"]},"title":"Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs","citation":{"apa":"Chatterjee, K., Fu, H., Novotný, P., & 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. https://doi.org/10.1145/2837614.2837639","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:10.1145/2837614.2837639","short":"K. Chatterjee, H. Fu, P. Novotný, R. Hasheminezhad, in:, ACM, 2016, pp. 327–342.","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.","mla":"Chatterjee, Krishnendu, et al. Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs. Vol. 20–22, ACM, 2016, pp. 327–42, doi:10.1145/2837614.2837639.","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. https://doi.org/10.1145/2837614.2837639."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","publisher":"ACM","oa":1,"acknowledgement":"Supported by the Natural Science Foundation of China (NSFC) under Grant No. 61532019 ","page":"327 - 342","doi":"10.1145/2837614.2837639","date_published":"2016-01-11T00:00:00Z","date_created":"2018-12-11T11:52:01Z","year":"2016","day":"11"},{"title":"Long-run average behaviour of probabilistic vector addition systems","department":[{"_id":"KrCh"}],"author":[{"first_name":"Tomáš","last_name":"Brázdil","full_name":"Brázdil, Tomáš"},{"full_name":"Kiefer, Stefan","last_name":"Kiefer","first_name":"Stefan"},{"first_name":"Antonín","full_name":"Kučera, Antonín","last_name":"Kučera"},{"last_name":"Novotny","full_name":"Novotny, Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","first_name":"Petr"}],"publist_id":"5490","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","date_updated":"2021-01-12T06:52:20Z","citation":{"chicago":"Brázdil, Tomáš, Stefan Kiefer, Antonín Kučera, and Petr Novotný. “Long-Run Average Behaviour of Probabilistic Vector Addition Systems,” 44–55. IEEE, 2015. https://doi.org/10.1109/LICS.2015.15.","ista":"Brázdil T, Kiefer S, Kučera A, Novotný P. 2015. Long-run average behaviour of probabilistic vector addition systems. LICS: Logic in Computer Science, LICS, , 44–55.","mla":"Brázdil, Tomáš, et al. Long-Run Average Behaviour of Probabilistic Vector Addition Systems. IEEE, 2015, pp. 44–55, doi:10.1109/LICS.2015.15.","short":"T. Brázdil, S. Kiefer, A. Kučera, P. Novotný, in:, IEEE, 2015, pp. 44–55.","ieee":"T. Brázdil, S. Kiefer, A. Kučera, and P. Novotný, “Long-run average behaviour of probabilistic vector addition systems,” presented at the LICS: Logic in Computer Science, Kyoto, Japan, 2015, pp. 44–55.","ama":"Brázdil T, Kiefer S, Kučera A, Novotný P. Long-run average behaviour of probabilistic vector addition systems. In: IEEE; 2015:44-55. doi:10.1109/LICS.2015.15","apa":"Brázdil, T., Kiefer, S., Kučera, A., & Novotný, P. (2015). Long-run average behaviour of probabilistic vector addition systems (pp. 44–55). Presented at the LICS: Logic in Computer Science, Kyoto, Japan: IEEE. https://doi.org/10.1109/LICS.2015.15"},"status":"public","project":[{"name":"International IST Postdoc Fellowship Programme","grant_number":"291734","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"conference":{"location":"Kyoto, Japan","end_date":"2015-07-10","start_date":"2015-07-06","name":"LICS: Logic in Computer Science"},"type":"conference","_id":"1660","ec_funded":1,"date_created":"2018-12-11T11:53:19Z","date_published":"2015-07-01T00:00:00Z","doi":"10.1109/LICS.2015.15","page":"44 - 55","language":[{"iso":"eng"}],"day":"01","publication_status":"published","year":"2015","month":"07","main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1505.02655"}],"oa":1,"scopus_import":1,"alternative_title":["LICS"],"quality_controlled":"1","publisher":"IEEE","oa_version":"Preprint","abstract":[{"lang":"eng","text":"We study the pattern frequency vector for runs in probabilistic Vector Addition Systems with States (pVASS). Intuitively, each configuration of a given pVASS is assigned one of finitely many patterns, and every run can thus be seen as an infinite sequence of these patterns. The pattern frequency vector assigns to each run the limit of pattern frequencies computed for longer and longer prefixes of the run. If the limit does not exist, then the vector is undefined. We show that for one-counter pVASS, the pattern frequency vector is defined and takes one of finitely many values for almost all runs. Further, these values and their associated probabilities can be approximated up to an arbitrarily small relative error in polynomial time. For stable two-counter pVASS, we show the same result, but we do not provide any upper complexity bound. As a byproduct of our study, we discover counterexamples falsifying some classical results about stochastic Petri nets published in the 80s."}]},{"date_updated":"2021-01-12T06:52:24Z","department":[{"_id":"KrCh"}],"series_title":"Lecture Notes in Computer Science","_id":"1667","type":"conference","conference":{"end_date":"2015-09-03","location":"Madrid, Spain","start_date":"2015-09-01","name":"QEST: Quantitative Evaluation of Systems"},"status":"public","publication_status":"published","language":[{"iso":"eng"}],"volume":9259,"ec_funded":1,"abstract":[{"text":"We consider parametric version of fixed-delay continuoustime Markov chains (or equivalently deterministic and stochastic Petri nets, DSPN) where fixed-delay transitions are specified by parameters, rather than concrete values. Our goal is to synthesize values of these parameters that, for a given cost function, minimise expected total cost incurred before reaching a given set of target states. We show that under mild assumptions, optimal values of parameters can be effectively approximated using translation to a Markov decision process (MDP) whose actions correspond to discretized values of these parameters. To this end we identify and overcome several interesting phenomena arising in systems with fixed delays.","lang":"eng"}],"oa_version":"Preprint","scopus_import":1,"alternative_title":["LNCS"],"main_file_link":[{"open_access":"1","url":"http://arxiv.org/abs/1407.4777"}],"month":"08","intvolume":" 9259","citation":{"chicago":"Brázdil, Tomáš, L’Uboš Korenčiak, Jan Krčál, Petr Novotný, and Vojtěch Řehák. “Optimizing Performance of Continuous-Time Stochastic Systems Using Timeout Synthesis.” Lecture Notes in Computer Science. Springer, 2015. https://doi.org/10.1007/978-3-319-22264-6_10.","ista":"Brázdil T, Korenčiak L, Krčál J, Novotný P, Řehák V. 2015. Optimizing performance of continuous-time stochastic systems using timeout synthesis. 9259, 141–159.","mla":"Brázdil, Tomáš, et al. Optimizing Performance of Continuous-Time Stochastic Systems Using Timeout Synthesis. Vol. 9259, Springer, 2015, pp. 141–59, doi:10.1007/978-3-319-22264-6_10.","apa":"Brázdil, T., Korenčiak, L., Krčál, J., Novotný, P., & Řehák, V. (2015). Optimizing performance of continuous-time stochastic systems using timeout synthesis. Presented at the QEST: Quantitative Evaluation of Systems, Madrid, Spain: Springer. https://doi.org/10.1007/978-3-319-22264-6_10","ama":"Brázdil T, Korenčiak L, Krčál J, Novotný P, Řehák V. Optimizing performance of continuous-time stochastic systems using timeout synthesis. 2015;9259:141-159. doi:10.1007/978-3-319-22264-6_10","ieee":"T. Brázdil, L. Korenčiak, J. Krčál, P. Novotný, and V. Řehák, “Optimizing performance of continuous-time stochastic systems using timeout synthesis,” vol. 9259. Springer, pp. 141–159, 2015.","short":"T. Brázdil, L. Korenčiak, J. Krčál, P. Novotný, V. Řehák, 9259 (2015) 141–159."},"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publist_id":"5482","author":[{"first_name":"Tomáš","full_name":"Brázdil, Tomáš","last_name":"Brázdil"},{"first_name":"L'Uboš","full_name":"Korenčiak, L'Uboš","last_name":"Korenčiak"},{"first_name":"Jan","full_name":"Krčál, Jan","last_name":"Krčál"},{"first_name":"Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","last_name":"Novotny","full_name":"Novotny, Petr"},{"first_name":"Vojtěch","full_name":"Řehák, Vojtěch","last_name":"Řehák"}],"title":"Optimizing performance of continuous-time stochastic systems using timeout synthesis","project":[{"grant_number":"291734","name":"International IST Postdoc Fellowship Programme","_id":"25681D80-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"}],"year":"2015","day":"22","page":"141 - 159","doi":"10.1007/978-3-319-22264-6_10","date_published":"2015-08-22T00:00:00Z","date_created":"2018-12-11T11:53:22Z","acknowledgement":"The research leading to these results has received funding from the People Programme (Marie Curie Actions) of the European Union’s Seventh Framework Programme (FP7/2007-2013) under REA grant agreement n∘ [291734]. This work is partly supported by the German Research Council (DFG) as part of the Transregional Collaborative Research Center AVACS (SFB/TR 14), by the EU 7th Framework Programme under grant agreement no. 295261 (MEALS) and 318490 (SENSATION), by the Czech Science Foundation, grant No. 15-17564S, and by the CAS/SAFEA International Partnership Program for Creative Research Teams.","publisher":"Springer","quality_controlled":"1","oa":1},{"abstract":[{"text":"We introduce consumption games, a model for discrete interactive system with multiple resources that are consumed or reloaded independently. More precisely, a consumption game is a finite-state graph where each transition is labeled by a vector of resource updates, where every update is a non-positive number or ω. The ω updates model the reloading of a given resource. Each vertex belongs either to player □ or player ◇, where the aim of player □ is to play so that the resources are never exhausted. We consider several natural algorithmic problems about consumption games, and show that although these problems are computationally hard in general, they are solvable in polynomial time for every fixed number of resource types (i.e., the dimension of the update vectors) and bounded resource updates. ","lang":"eng"}],"oa_version":"Preprint","main_file_link":[{"url":"http://arxiv.org/abs/1202.0796","open_access":"1"}],"alternative_title":["LNCS"],"scopus_import":1,"intvolume":" 7358","month":"07","publication_status":"published","language":[{"iso":"eng"}],"ec_funded":1,"volume":7358,"_id":"3135","conference":{"name":"CAV: Computer Aided Verification","end_date":"2012-07-13","location":"Berkeley, CA, USA","start_date":"2012-07-07"},"type":"conference","status":"public","date_updated":"2021-01-12T07:41:18Z","department":[{"_id":"KrCh"}],"acknowledgement":"Tomas Brazdil, Antonin Kucera, and Petr Novotny are supported by the Czech Science Foundation, grant No. P202/10/1469. Krishnendu Chatterjee is supported by the FWF (Austrian Science Fund) NFN Grant No S11407-N23 (RiSE) and ERC Start grant (279307: Graph Games).","oa":1,"publisher":"Springer","quality_controlled":"1","year":"2012","day":"01","page":"23 - 38","date_created":"2018-12-11T12:01:35Z","date_published":"2012-07-01T00:00:00Z","doi":"10.1007/978-3-642-31424-7_8","project":[{"grant_number":"279307","name":"Quantitative Graph Games: Theory and Applications","_id":"2581B60A-B435-11E9-9278-68D0E5697425","call_identifier":"FP7"},{"grant_number":"S 11407_N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25832EC2-B435-11E9-9278-68D0E5697425"}],"citation":{"ista":"Brázdil B, Chatterjee K, Kučera A, Novotný P. 2012. Efficient controller synthesis for consumption games with multiple resource types. CAV: Computer Aided Verification, LNCS, vol. 7358, 23–38.","chicago":"Brázdil, Brázdil, Krishnendu Chatterjee, Antonín Kučera, and Petr Novotný. “Efficient Controller Synthesis for Consumption Games with Multiple Resource Types,” 7358:23–38. Springer, 2012. https://doi.org/10.1007/978-3-642-31424-7_8.","ieee":"B. Brázdil, K. Chatterjee, A. Kučera, and P. Novotný, “Efficient controller synthesis for consumption games with multiple resource types,” presented at the CAV: Computer Aided Verification, Berkeley, CA, USA, 2012, vol. 7358, pp. 23–38.","short":"B. Brázdil, K. Chatterjee, A. Kučera, P. Novotný, in:, Springer, 2012, pp. 23–38.","apa":"Brázdil, B., Chatterjee, K., Kučera, A., & Novotný, P. (2012). Efficient controller synthesis for consumption games with multiple resource types (Vol. 7358, pp. 23–38). Presented at the CAV: Computer Aided Verification, Berkeley, CA, USA: Springer. https://doi.org/10.1007/978-3-642-31424-7_8","ama":"Brázdil B, Chatterjee K, Kučera A, Novotný P. Efficient controller synthesis for consumption games with multiple resource types. In: Vol 7358. Springer; 2012:23-38. doi:10.1007/978-3-642-31424-7_8","mla":"Brázdil, Brázdil, et al. Efficient Controller Synthesis for Consumption Games with Multiple Resource Types. Vol. 7358, Springer, 2012, pp. 23–38, doi:10.1007/978-3-642-31424-7_8."},"user_id":"3E5EF7F0-F248-11E8-B48F-1D18A9856A87","publist_id":"3562","author":[{"first_name":"Brázdil","last_name":"Brázdil","full_name":"Brázdil, Brázdil"},{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","first_name":"Krishnendu","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X"},{"last_name":"Kučera","full_name":"Kučera, Antonín","first_name":"Antonín"},{"last_name":"Novotny","full_name":"Novotny, Petr","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","first_name":"Petr"}],"title":"Efficient controller synthesis for consumption games with multiple resource types"}]