New approaches for almost-sure termination of probabilistic programs

Huang, Mingzhang; Fu, Hongfei; Chatterjee, Krishnendu

New approaches for almost-sure termination of probabilistic programs

Huang M, Fu H, Chatterjee K. 2018. New approaches for almost-sure termination of probabilistic programs. 16th Asian Symposium on Programming Languages and Systems, APLAS, LNCS, vol. 11275, 181–201.

Download (ext.)

http://arxiv.org/abs/1806.06683 [Preprint]

DOI

10.1007/978-3-030-02768-1_11

Conference Paper | English

Scopus indexed

Author

Huang, Mingzhang; Fu, Hongfei; Chatterjee, Krishnendu^ISTA

Editor

Ryu, Sukyoung

Department

Chatterjee Group

Grant

Rigorous Systems Engineering
Efficient Algorithms for Computer Aided Verification

Series Title

LNCS

Abstract

We study the almost-sure termination problem for probabilistic programs. First, we show that supermartingales with lower bounds on conditional absolute difference provide a sound approach for the almost-sure termination problem. Moreover, using this approach we can obtain explicit optimal bounds on tail probabilities of non-termination within a given number of steps. Second, we present a new approach based on Central Limit Theorem for the almost-sure termination problem, and show that this approach can establish almost-sure termination of programs which none of the existing approaches can handle. Finally, we discuss algorithmic approaches for the two above methods that lead to automated analysis techniques for almost-sure termination of probabilistic programs.

Publishing Year

2018

Date Published

2018-12-01

Publisher

Springer

Volume

11275

Page

181-201

Conference

16th Asian Symposium on Programming Languages and Systems, APLAS

Conference Location

Wellington, New Zealand

Conference Date

2018-12-02 – 2018-12-06

ISBN

9783030027674

ISSN

03029743

IST-REx-ID

5679

Cite this

Huang M, Fu H, Chatterjee K. New approaches for almost-sure termination of probabilistic programs. In: Ryu S, ed. Vol 11275. Springer; 2018:181-201. doi:10.1007/978-3-030-02768-1_11

Huang, M., Fu, H., & Chatterjee, K. (2018). New approaches for almost-sure termination of probabilistic programs. In S. Ryu (Ed.) (Vol. 11275, pp. 181–201). Presented at the 16th Asian Symposium on Programming Languages and Systems, APLAS, Wellington, New Zealand: Springer. https://doi.org/10.1007/978-3-030-02768-1_11

Huang, Mingzhang, Hongfei Fu, and Krishnendu Chatterjee. “New Approaches for Almost-Sure Termination of Probabilistic Programs.” edited by Sukyoung Ryu, 11275:181–201. Springer, 2018. https://doi.org/10.1007/978-3-030-02768-1_11.

M. Huang, H. Fu, and K. Chatterjee, “New approaches for almost-sure termination of probabilistic programs,” presented at the 16th Asian Symposium on Programming Languages and Systems, APLAS, Wellington, New Zealand, 2018, vol. 11275, pp. 181–201.

Huang M, Fu H, Chatterjee K. 2018. New approaches for almost-sure termination of probabilistic programs. 16th Asian Symposium on Programming Languages and Systems, APLAS, LNCS, vol. 11275, 181–201.

Huang, Mingzhang, et al. New Approaches for Almost-Sure Termination of Probabilistic Programs. Edited by Sukyoung Ryu, vol. 11275, Springer, 2018, pp. 181–201, doi:10.1007/978-3-030-02768-1_11.

All files available under the following license(s):

Copyright Statement: