Termination Analysis of Probabilistic Programs with Martingales

C 2020

Termination Analysis of Probabilistic Programs with Martingales

CHATTERJEE, Krishnendu, Hongfei FU a Petr NOVOTNÝ

Základní údaje

Originální název

Termination Analysis of Probabilistic Programs with Martingales

Autoři

CHATTERJEE, Krishnendu (356 Indie), Hongfei FU (156 Čína) a Petr NOVOTNÝ (203 Česká republika, garant, domácí)

Vydání

Cambridge, UK, Foundations of Probabilistic Programming, od s. 221-258, 38 s. 2020

Nakladatel

Cambridge University Press

Další údaje

Jazyk

angličtina

Typ výsledku

Kapitola resp. kapitoly v odborné knize

Obor

10200 1.2 Computer and information sciences

Stát vydavatele

Velká Británie a Severní Irsko

Utajení

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

Forma vydání

tištěná verze "print"

Kód RIV

RIV/00216224:14330/20:00114618

Organizační jednotka

Fakulta informatiky

ISBN

978-1-108-48851-8

DOI

http://dx.doi.org/10.1017/9781108770750.008

Klíčová slova anglicky

probabilistic programs; program analysis; termination; martingales

Štítky

formela-ver, topvydavatel

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 28. 4. 2021 19:16, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

Probabilistic programs extend classical imperative programs with random-value generators. For classical non-probabilistic programs, termination is a key question in static analysis of programs, that given a program and an initial condition asks whether it terminates. In the presence of probabilistic behavior there are two fundamental extensions of the termination question, namely, (a) the almost-sure termination question that asks whether the termination probability is 1; and (b) the bounded-time termination question that asks whether the expected termination time is bounded. While there are many active research directions to address the above problems, one important research direction is the use of martingale theory for termination analysis. We will survey the main techniques related to martingale-based approach for termination analysis of probabilistic programs.

Návaznosti

GA19-15134Y, interní kód MU

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

Investor: Grantová agentura ČR, Verifikace a analýza pravděpodobnostních programů

GJ19-15134Y, projekt VaV

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

Citovat

CHATTERJEE, Krishnendu, Hongfei FU a Petr NOVOTNÝ. Termination Analysis of Probabilistic Programs with Martingales. In Gilles Barthe, Joost-Pieter Katoen, Alexandra Silva. Foundations of Probabilistic Programming. Cambridge, UK: Cambridge University Press, 2020, s. 221-258. ISBN 978-1-108-48851-8. Dostupné z: https://dx.doi.org/10.1017/9781108770750.008.

@inbook{1718657,
   author = {Chatterjee, Krishnendu and Fu, Hongfei and Novotný, Petr},
   address = {Cambridge, UK},
   booktitle = {Foundations of Probabilistic Programming},
   doi = {http://dx.doi.org/10.1017/9781108770750.008},
   editor = {Gilles Barthe, Joost-Pieter Katoen, Alexandra Silva},
   keywords = {probabilistic programs; program analysis; termination; martingales},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Cambridge, UK},
   isbn = {978-1-108-48851-8},
   pages = {221-258},
   publisher = {Cambridge University Press},
   title = {Termination Analysis of Probabilistic Programs with Martingales},
   year = {2020}
}

TY  - CHAP
ID  - 1718657
AU  - Chatterjee, Krishnendu - Fu, Hongfei - Novotný, Petr
PY  - 2020
TI  - Termination Analysis of Probabilistic Programs with Martingales
VL  - Neuveden
PB  - Cambridge University Press
CY  - Cambridge, UK
SN  - 9781108488518
KW  - probabilistic programs
KW  - program analysis
KW  - termination
KW  - martingales
N2  - Probabilistic programs extend classical imperative programs with random-value generators. For classical non-probabilistic programs, termination is a key question in static analysis of programs, that given a program and an initial condition asks whether it terminates. In the presence of probabilistic behavior there are two fundamental extensions of the termination question, namely, (a) the almost-sure termination question that asks whether the termination probability is 1; and (b) the bounded-time termination question that asks whether the expected termination time is bounded. While there are many active research directions to address the above problems, one important research direction is the use of martingale theory for termination analysis. We will survey the main techniques related to martingale-based approach for termination analysis of probabilistic programs.
ER  -

CHATTERJEE, Krishnendu, Hongfei FU a Petr NOVOTNÝ. Termination Analysis of Probabilistic Programs with Martingales. In Gilles Barthe, Joost-Pieter Katoen, Alexandra Silva. \textit{Foundations of Probabilistic Programming}. Cambridge, UK: Cambridge University Press, 2020, s.~221-258. ISBN~978-1-108-48851-8. Dostupné z: https://dx.doi.org/10.1017/9781108770750.008.

Podrobný výpis o publikaci