CHATTERJEE, Krishnendu, Hongfei FU and 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, p. 221-258. ISBN 978-1-108-48851-8. Available from: https://dx.doi.org/10.1017/9781108770750.008.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name Termination Analysis of Probabilistic Programs with Martingales
Authors CHATTERJEE, Krishnendu (356 India), Hongfei FU (156 China) and Petr NOVOTNÝ (203 Czech Republic, guarantor, belonging to the institution).
Edition Cambridge, UK, Foundations of Probabilistic Programming, p. 221-258, 38 pp. 2020.
Publisher Cambridge University Press
Other information
Original language English
Type of outcome Chapter(s) of a specialized book
Field of Study 10200 1.2 Computer and information sciences
Country of publisher United Kingdom of Great Britain and Northern Ireland
Confidentiality degree is not subject to a state or trade secret
Publication form printed version "print"
RIV identification code RIV/00216224:14330/20:00114618
Organization unit Faculty of Informatics
ISBN 978-1-108-48851-8
Doi http://dx.doi.org/10.1017/9781108770750.008
Keywords in English probabilistic programs; program analysis; termination; martingales
Tags formela-ver, topvydavatel
Tags International impact, Reviewed
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 28/4/2021 19:16.
Abstract
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.
Links
GA19-15134Y, interní kód MUName: Verifikace a analýza pravděpodobnostních programů
Investor: Czech Science Foundation
GJ19-15134Y, research and development projectName: Verifikace a analýza pravděpodobnostních programů
PrintDisplayed: 25/5/2024 20:16