Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time

P. Wang, H. Fu, K. Chatterjee, Y. Deng, M. Xu, in:, Proceedings of the ACM on Programming Languages, ACM, 2019.

Download
OA 2019_ACM_POPL_Wang.pdf 564.15 KB

Conference Paper | Published | English

Scopus indexed
Author
Wang, Peixin; Fu, Hongfei; Chatterjee, KrishnenduIST Austria ; Deng, Yuxin; Xu, Ming
Abstract
The notion of program sensitivity (aka Lipschitz continuity) specifies that changes in the program input result in proportional changes to the program output. For probabilistic programs the notion is naturally extended to expected sensitivity. A previous approach develops a relational program logic framework for proving expected sensitivity of probabilistic while loops, where the number of iterations is fixed and bounded. In this work, we consider probabilistic while loops where the number of iterations is not fixed, but randomized and depends on the initial input values. We present a sound approach for proving expected sensitivity of such programs. Our sound approach is martingale-based and can be automated through existing martingale-synthesis algorithms. Furthermore, our approach is compositional for sequential composition of while loops under a mild side condition. We demonstrate the effectiveness of our approach on several classical examples from Gambler's Ruin, stochastic hybrid systems and stochastic gradient descent. We also present experimental results showing that our automated approach can handle various probabilistic programs in the literature.
Publishing Year
Date Published
2019-12-01
Proceedings Title
Proceedings of the ACM on Programming Languages
Acknowledgement
We thank anonymous reviewers for helpful comments, especially for pointing to us a scenario of piecewise-linear approximation (Remark5). The research was partially supported by the National Natural Science Foundation of China (NSFC) under Grant No. 61802254, 61672229, 61832015,61772336,11871221 and Austrian Science Fund (FWF) NFN under Grant No. S11407-N23 (RiSE/SHiNE). We thank Prof. Yuxi Fu, director of the BASICS Lab at Shanghai Jiao Tong University, for his support.
Volume
4
Issue
POPL
Article Number
25
eISSN
IST-REx-ID

Cite this

Wang P, Fu H, Chatterjee K, Deng Y, Xu M. Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time. In: Proceedings of the ACM on Programming Languages. Vol 4. ACM; 2019. doi:10.1145/3371093
Wang, P., Fu, H., Chatterjee, K., Deng, Y., & Xu, M. (2019). Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time. In Proceedings of the ACM on Programming Languages (Vol. 4). ACM. https://doi.org/10.1145/3371093
Wang, Peixin, Hongfei Fu, Krishnendu Chatterjee, Yuxin Deng, and Ming Xu. “Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time.” In Proceedings of the ACM on Programming Languages, Vol. 4. ACM, 2019. https://doi.org/10.1145/3371093.
P. Wang, H. Fu, K. Chatterjee, Y. Deng, and M. Xu, “Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time,” in Proceedings of the ACM on Programming Languages, 2019, vol. 4, no. POPL.
Wang P, Fu H, Chatterjee K, Deng Y, Xu M. 2019. Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time. Proceedings of the ACM on Programming Languages. vol. 4.
Wang, Peixin, et al. “Proving Expected Sensitivity of Probabilistic Programs with Randomized Variable-Dependent Termination Time.” Proceedings of the ACM on Programming Languages, vol. 4, no. POPL, 25, ACM, 2019, doi:10.1145/3371093.
All files available under the following license(s):
Creative Commons Attribution 4.0 International Public License (CC-BY 4.0):
Main File(s)
File Name
Access Level
OA Open Access
Date Uploaded
2020-09-01
MD5 Checksum
c6193d109ff4ecb17e7a6513d8eb34c0


Export

Marked Publications

Open Data IST Research Explorer

Sources

arXiv 1902.04744v3

Search this title in

Google Scholar