On Lexicographic Proof Rules for Probabilistic Termination

D 2021

On Lexicographic Proof Rules for Probabilistic Termination

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

Basic information

Original name

On Lexicographic Proof Rules for Probabilistic Termination

Authors

CHATTERJEE, Krishnendu (356 India), Ehsan Kafshdar GOHARSHADY (364 Islamic Republic of Iran), Petr NOVOTNÝ (203 Czech Republic, guarantor, belonging to the institution), Jiří ZÁREVÚCKY (203 Czech Republic, belonging to the institution) and Djordje ŽIKELIĆ (688 Serbia)

Edition

Cham, Switzerland, 24th International Symposium on Formal Methods, FM 2021, p. 619-639, 21 pp. 2021

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Confidentiality degree

není předmětem státního či obchodního tajemství

Publication form

electronic version available online

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/21:00119268

Organization unit

Faculty of Informatics

ISBN

978-3-030-90869-0

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-90870-6_33

UT WoS

000758218600033

Keywords in English

program analysis; probabilistic programs; almost-sure termination; martingales

Abstract

V originále

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.

Links

GJ19-15134Y, research and development project

Name: Verifikace a analýza pravděpodobnostních programů

Citovat

CHATTERJEE, Krishnendu, Ehsan Kafshdar GOHARSHADY, Petr NOVOTNÝ, Jiří ZÁREVÚCKY and Djordje ŽIKELIĆ. On Lexicographic Proof Rules for Probabilistic Termination. Online. In 24th International Symposium on Formal Methods, FM 2021. Cham, Switzerland: Springer, 2021, p. 619-639. ISBN 978-3-030-90869-0. Available from: https://dx.doi.org/10.1007/978-3-030-90870-6_33.

@inproceedings{1797365,
   author = {Chatterjee, Krishnendu and Goharshady, Ehsan Kafshdar and Novotný, Petr and Zárevúcky, Jiří and Žikelić, Djordje},
   address = {Cham, Switzerland},
   booktitle = {24th International Symposium on Formal Methods, FM 2021},
   doi = {http://dx.doi.org/10.1007/978-3-030-90870-6_33},
   keywords = {program analysis; probabilistic programs; almost-sure termination; martingales},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Cham, Switzerland},
   isbn = {978-3-030-90869-0},
   pages = {619-639},
   publisher = {Springer},
   title = {On Lexicographic Proof Rules for Probabilistic Termination},
   year = {2021}
}

TY  - JOUR
ID  - 1797365
AU  - Chatterjee, Krishnendu - Goharshady, Ehsan Kafshdar - Novotný, Petr - Zárevúcky, Jiří - Žikelić, Djordje
PY  - 2021
TI  - On Lexicographic Proof Rules for Probabilistic Termination
PB  - Springer
CY  - Cham, Switzerland
SN  - 9783030908690
KW  - program analysis
KW  - probabilistic programs
KW  - almost-sure termination
KW  - martingales
N2  - 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.
ER  -

CHATTERJEE, Krishnendu, Ehsan Kafshdar GOHARSHADY, Petr NOVOTNÝ, Jiří ZÁREVÚCKY and Djordje ŽIKELI$\backslash$'C. On Lexicographic Proof Rules for Probabilistic Termination. Online. In \textit{24th International Symposium on Formal Methods, FM 2021}. Cham, Switzerland: Springer, 2021, p.~619-639. ISBN~978-3-030-90869-0. Available from: https://dx.doi.org/10.1007/978-3-030-90870-6\_{}33.

Detailed Information on Publication Record