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.

Základní údaje

Originální název

On Lexicographic Proof Rules for Probabilistic Termination

Autoři

CHATTERJEE, Krishnendu (356 Indie), Ehsan Kafshdar GOHARSHADY (364 Írán), Petr NOVOTNÝ (203 Česká republika, garant, domácí), Jiří ZÁREVÚCKY (203 Česká republika, domácí) a Djordje ŽIKELIĆ (688 Srbsko)

Vydání

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

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Utajení

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

Forma vydání

elektronická verze "online"

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/21:00119268

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-90869-0

ISSN

DOI

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

UT WoS

000758218600033

Klíčová slova anglicky

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

Štítky

core_A, firank_A, formela-ver

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 28. 4. 2022 10:00, RNDr. Pavel Šmerk, Ph.D.

Anotace

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.

Návaznosti

GJ19-15134Y, projekt VaV

Název: Verifikace a analýza pravděpodobnostních programů

Citovat

CHATTERJEE, Krishnendu, Ehsan Kafshdar GOHARSHADY, Petr NOVOTNÝ, Jiří ZÁREVÚCKY a Djordje ŽIKELIĆ. On Lexicographic Proof Rules for Probabilistic Termination. Online. In 24th International Symposium on Formal Methods, FM 2021. Cham, Switzerland: Springer, 2021, s. 619-639. ISBN 978-3-030-90869-0. Dostupné z: 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 a 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, s.~619-639. ISBN~978-3-030-90869-0. Dostupné z: https://dx.doi.org/10.1007/978-3-030-90870-6\_{}33.

Podrobný výpis o publikaci