[{"doi":"10.1145/3585391","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publication":"Formal Aspects of Computing","day":"23","article_number":"11","ec_funded":1,"article_type":"original","keyword":["Theoretical Computer Science","Software"],"oa":1,"publication_identifier":{"issn":["0934-5043"],"eissn":["1433-299X"]},"language":[{"iso":"eng"}],"project":[{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","grant_number":"863818","call_identifier":"H2020"},{"grant_number":"665385","name":"International IST Doctoral Program","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020"}],"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.","year":"2023","department":[{"_id":"KrCh"}],"arxiv":1,"title":"On lexicographic proof rules for probabilistic termination","date_updated":"2025-07-14T09:10:10Z","oa_version":"Published Version","ddc":["000"],"month":"06","status":"public","tmp":{"legal_code_url":"https://creativecommons.org/licenses/by/4.0/legalcode","short":"CC BY (4.0)","image":"/images/cc_by.png","name":"Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)"},"related_material":{"record":[{"id":"10414","relation":"earlier_version","status":"public"}]},"file":[{"file_name":"2023_FormalAspectsComputing_Chatterjee.pdf","file_size":502522,"success":1,"date_updated":"2024-01-16T08:11:24Z","content_type":"application/pdf","relation":"main_file","file_id":"14804","creator":"dernst","checksum":"3bb133eeb27ec01649a9a36445d952d9","date_created":"2024-01-16T08:11:24Z","access_level":"open_access"}],"type":"journal_article","article_processing_charge":"Yes (via OA deal)","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>.","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.","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>","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>","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.","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>.","short":"K. Chatterjee, E. Kafshdar Goharshady, P. Novotný, J. Zárevúcky, D. Zikelic, Formal Aspects of Computing 35 (2023)."},"has_accepted_license":"1","publisher":"Association for Computing Machinery","license":"https://creativecommons.org/licenses/by/4.0/","issue":"2","quality_controlled":"1","_id":"14778","date_published":"2023-06-23T00:00:00Z","intvolume":"        35","author":[{"full_name":"Chatterjee, Krishnendu","orcid":"0000-0002-4561-241X","first_name":"Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","last_name":"Chatterjee"},{"first_name":"Ehsan","full_name":"Kafshdar Goharshady, Ehsan","last_name":"Kafshdar Goharshady"},{"last_name":"Novotný","id":"3CC3B868-F248-11E8-B48F-1D18A9856A87","full_name":"Novotný, Petr","first_name":"Petr"},{"full_name":"Zárevúcky, Jiří","first_name":"Jiří","last_name":"Zárevúcky"},{"last_name":"Zikelic","full_name":"Zikelic, Dorde","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","first_name":"Dorde","orcid":"0000-0002-4681-1699"}],"volume":35,"date_created":"2024-01-10T09:27:43Z","publication_status":"published","external_id":{"arxiv":["2108.02188"]},"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."}],"file_date_updated":"2024-01-16T08:11:24Z"}]