On Lexicographic Proof Rules for Probabilistic Termination

Logo poskytovatele

Varování

Publikace nespadá pod Filozofickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

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

Rok publikování 2023
Druh Článek v odborném periodiku
Časopis / Zdroj Formal Aspects of Computing
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
www https://dl.acm.org/doi/10.1145/3585391
Doi http://dx.doi.org/10.1145/3585391
Klíčová slova probabilistic programs; termination; martingales
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.