On lexicographic proof rules for probabilistic termination

conference paper On lexicographic proof rules for probabilistic termination LNCS published yes Krishnendu Chatterjee author 2E5DCA20-F248-11E8-B48F-1D18A9856A870000-0002-4561-241X Ehsan Kafshdar Goharshadi author 103b4fa0-896a-11ed-bdf8-87b697bef40d0000-0002-8595-0587 Petr Novotný author 3CC3B868-F248-11E8-B48F-1D18A9856A87 Jiří Zárevúcky author Dorde Zikelic author 294AA7A6-F248-11E8-B48F-1D18A9856A870000-0002-4681-1699 KrCh department FM: Formal Methods Formal Methods for Stochastic Models: Algorithms and Applications project International IST Doctoral Program project 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. Springer Nature2021Virtual eng 24th International Symposium on Formal Methods 0302-9743 1611-3349 9-783-0309-0869-0 2108.02188 00075821860003310.1007/978-3-030-90870-6_33 13047619-639 https://research-explorer.ista.ac.at/record/14778 https://research-explorer.ista.ac.at/record/14539 Chatterjee K, Goharshady E, Novotný P, Zárevúcky J, Zikelic D. 2021. On lexicographic proof rules for probabilistic termination. 24th International Symposium on Formal Methods. FM: Formal Methods, LNCS, vol. 13047, 619–639. Chatterjee K, Goharshady E, 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:<a href="https://doi.org/10.1007/978-3-030-90870-6_33">10.1007/978-3-030-90870-6_33</a> Chatterjee, K., Goharshady, E., 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. <a href="https://doi.org/10.1007/978-3-030-90870-6_33">https://doi.org/10.1007/978-3-030-90870-6_33</a> Chatterjee, Krishnendu, Ehsan 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. <a href="https://doi.org/10.1007/978-3-030-90870-6_33">https://doi.org/10.1007/978-3-030-90870-6_33</a>. K. Chatterjee, E. 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. 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:<a href="https://doi.org/10.1007/978-3-030-90870-6_33">10.1007/978-3-030-90870-6_33</a>. K. Chatterjee, E. Goharshady, P. Novotný, J. Zárevúcky, D. Zikelic, in:, 24th International Symposium on Formal Methods, Springer Nature, 2021, pp. 619–639. 104142021-12-05T23:01:45Z2026-04-07T13:27:55Z