On lexicographic proof rules for probabilistic termination

Chatterjee K, Goharshady EK, Novotný P, Zárevúcky J, Žikelić Đ. 2021. On lexicographic proof rules for probabilistic termination. 24th International Symposium on Formal Methods. FM: Formal Methods, LNCS, vol. 13047, 619–639.


Conference Paper | Published | English

Scopus indexed
Author
Chatterjee, KrishnenduISTA ; Goharshady, Ehsan Kafshdar; Novotny, PetrISTA; Zárevúcky, Jiří; Žikelić, Đorđe
Department
Series Title
LNCS
Abstract
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.
Publishing Year
Date Published
2021-11-10
Proceedings Title
24th International Symposium on Formal Methods
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.
Volume
13047
Page
619-639
Conference
FM: Formal Methods
Conference Location
Virtual
Conference Date
2021-11-20 – 2021-11-26
ISSN
eISSN
IST-REx-ID

Cite this

Chatterjee K, Goharshady EK, Novotný P, Zárevúcky J, Žikelić Đ. 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
Chatterjee, K., Goharshady, E. K., Novotný, P., Zárevúcky, J., & Žikelić, Đ. (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
Chatterjee, Krishnendu, Ehsan Kafshdar Goharshady, Petr Novotný, Jiří Zárevúcky, and Đorđe Žikelić. “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.
K. Chatterjee, E. K. Goharshady, P. Novotný, J. Zárevúcky, and Đ. Žikelić, “On lexicographic proof rules for probabilistic termination,” in 24th International Symposium on Formal Methods, Virtual, 2021, vol. 13047, pp. 619–639.
Chatterjee K, Goharshady EK, Novotný P, Zárevúcky J, Žikelić Đ. 2021. On lexicographic proof rules for probabilistic termination. 24th International Symposium on Formal Methods. FM: Formal Methods, LNCS, vol. 13047, 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:10.1007/978-3-030-90870-6_33.
All files available under the following license(s):
Copyright Statement:
This Item is protected by copyright and/or related rights. [...]

Link(s) to Main File(s)
Access Level
OA Open Access

Export

Marked Publications

Open Data ISTA Research Explorer

Sources

arXiv 2108.02188

Search this title in

Google Scholar
ISBN Search