Sound and complete certificates for quantitative termination analysis of probabilistic programs
We consider the quantitative problem of obtaining lower-bounds on the probability of termination of a given non-deterministic probabilistic program. Specifically, given a non-termination threshold p∈[0,1], we aim for certificates proving that the program terminates with probability at least 1−p. The...
Saved in:
Main Authors: | , , , |
---|---|
Format: | text |
Language: | English |
Published: |
Institutional Knowledge at Singapore Management University
2022
|
Subjects: | |
Online Access: | https://ink.library.smu.edu.sg/sis_research/9076 https://ink.library.smu.edu.sg/context/sis_research/article/10079/viewcontent/sound.pdf |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Institution: | Singapore Management University |
Language: | English |
id |
sg-smu-ink.sis_research-10079 |
---|---|
record_format |
dspace |
spelling |
sg-smu-ink.sis_research-100792024-08-01T15:20:24Z Sound and complete certificates for quantitative termination analysis of probabilistic programs CHATTERJEE, Krishnendu GOHARSHADY, Amir Kafshdar MEGGENDORFER, Tobias ZIKELIC, Dorde We consider the quantitative problem of obtaining lower-bounds on the probability of termination of a given non-deterministic probabilistic program. Specifically, given a non-termination threshold p∈[0,1], we aim for certificates proving that the program terminates with probability at least 1−p. The basic idea of our approach is to find a terminating stochastic invariant, i.e. a subset SI of program states such that (i) the probability of the program ever leaving SI is no more than p, and (ii) almost-surely, the program either leaves SI or terminates.While stochastic invariants are already well-known, we provide the first proof that the idea above is not only sound, but also complete for quantitative termination analysis. We then introduce a novel sound and complete characterization of stochastic invariants that enables template-based approaches for easy synthesis of quantitative termination certificates, especially in affine or polynomial forms. Finally, by combining this idea with the existing martingale-based methods that are relatively complete for qualitative termination analysis, we obtain the first automated, sound, and relatively complete algorithm for quantitative termination analysis. Notably, our completeness guarantees for quantitative termination analysis are as strong as the best-known methods for the qualitative variant.Our prototype implementation demonstrates the effectiveness of our approach on various probabilistic programs. We also demonstrate that our algorithm certifies lower bounds on termination probability for probabilistic programs that are beyond the reach of previous methods. 2022-08-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/9076 info:doi/10.1007/978-3-031-13185-1_4 https://ink.library.smu.edu.sg/context/sis_research/article/10079/viewcontent/sound.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Programming Languages and Compilers |
institution |
Singapore Management University |
building |
SMU Libraries |
continent |
Asia |
country |
Singapore Singapore |
content_provider |
SMU Libraries |
collection |
InK@SMU |
language |
English |
topic |
Programming Languages and Compilers |
spellingShingle |
Programming Languages and Compilers CHATTERJEE, Krishnendu GOHARSHADY, Amir Kafshdar MEGGENDORFER, Tobias ZIKELIC, Dorde Sound and complete certificates for quantitative termination analysis of probabilistic programs |
description |
We consider the quantitative problem of obtaining lower-bounds on the probability of termination of a given non-deterministic probabilistic program. Specifically, given a non-termination threshold p∈[0,1], we aim for certificates proving that the program terminates with probability at least 1−p. The basic idea of our approach is to find a terminating stochastic invariant, i.e. a subset SI of program states such that (i) the probability of the program ever leaving SI is no more than p, and (ii) almost-surely, the program either leaves SI or terminates.While stochastic invariants are already well-known, we provide the first proof that the idea above is not only sound, but also complete for quantitative termination analysis. We then introduce a novel sound and complete characterization of stochastic invariants that enables template-based approaches for easy synthesis of quantitative termination certificates, especially in affine or polynomial forms. Finally, by combining this idea with the existing martingale-based methods that are relatively complete for qualitative termination analysis, we obtain the first automated, sound, and relatively complete algorithm for quantitative termination analysis. Notably, our completeness guarantees for quantitative termination analysis are as strong as the best-known methods for the qualitative variant.Our prototype implementation demonstrates the effectiveness of our approach on various probabilistic programs. We also demonstrate that our algorithm certifies lower bounds on termination probability for probabilistic programs that are beyond the reach of previous methods. |
format |
text |
author |
CHATTERJEE, Krishnendu GOHARSHADY, Amir Kafshdar MEGGENDORFER, Tobias ZIKELIC, Dorde |
author_facet |
CHATTERJEE, Krishnendu GOHARSHADY, Amir Kafshdar MEGGENDORFER, Tobias ZIKELIC, Dorde |
author_sort |
CHATTERJEE, Krishnendu |
title |
Sound and complete certificates for quantitative termination analysis of probabilistic programs |
title_short |
Sound and complete certificates for quantitative termination analysis of probabilistic programs |
title_full |
Sound and complete certificates for quantitative termination analysis of probabilistic programs |
title_fullStr |
Sound and complete certificates for quantitative termination analysis of probabilistic programs |
title_full_unstemmed |
Sound and complete certificates for quantitative termination analysis of probabilistic programs |
title_sort |
sound and complete certificates for quantitative termination analysis of probabilistic programs |
publisher |
Institutional Knowledge at Singapore Management University |
publishDate |
2022 |
url |
https://ink.library.smu.edu.sg/sis_research/9076 https://ink.library.smu.edu.sg/context/sis_research/article/10079/viewcontent/sound.pdf |
_version_ |
1814047724911198208 |