Termination Analysis of Probabilistic Programs with Martingales

Result code in 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>
Result on the web
<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>

Result language
angličtina
Original language name
Termination Analysis of Probabilistic Programs with Martingales
Original language description
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.
Czech name
—
Czech description
—

Project
<a href="/en/project/GJ19-15134Y" target="_blank" >GJ19-15134Y: Verification and Analysis of Probabilistic Programs</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

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

Similar results(10)