Termination Analysis of Probabilistic Programs with Martingales

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F20%3A00114618" target="_blank" >RIV/00216224:14330/20:00114618 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1017/9781108770750.008" target="_blank" >http://dx.doi.org/10.1017/9781108770750.008</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1017/9781108770750.008" target="_blank" >10.1017/9781108770750.008</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Termination Analysis of Probabilistic Programs with Martingales

Popis výsledku v původním jazyce

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ázev v anglickém jazyce

Termination Analysis of Probabilistic Programs with Martingales

Popis výsledku anglicky

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.

Druh

C - Kapitola v odborné knize

CEP obor

—

OECD FORD obor

10200 - Computer and information sciences

Projekt

<a href="/cs/project/GJ19-15134Y" target="_blank" >GJ19-15134Y: Verifikace a analýza pravděpodobnostních programů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2020

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název knihy nebo sborníku

Foundations of Probabilistic Programming

ISBN

9781108488518

Počet stran výsledku

38

Strana od-do

221-258

Počet stran knihy

582

Název nakladatele

Cambridge University Press

Místo vydání

Cambridge, UK

Kód UT WoS kapitoly

—