On Lexicographic Proof Rules for Probabilistic Termination

Investor logo

Warning

This publication doesn't include Faculty of Sports Studies. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

CHATTERJEE Krishnendu GOHARSHADY Ehsan Kafshdar NOVOTNÝ Petr ZÁREVÚCKY Jiří ŽIKELIĆ Djordje

Year of publication 2023
Type Article in Periodical
Magazine / Source Formal Aspects of Computing
MU Faculty or unit

Faculty of Informatics

Citation
Web https://dl.acm.org/doi/10.1145/3585391
Doi http://dx.doi.org/10.1145/3585391
Keywords probabilistic programs; termination; martingales
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.

More info