Termination analysis of probabilistic programs through Positivstellensatz's

K. Chatterjee, H. Fu, A. Goharshady, in:, Springer, 2016, pp. 3–22.


Conference Paper | Published | English
Department
Series Title
LNCS
Abstract
We consider nondeterministic probabilistic programs with the most basic liveness property of termination. We present efficient methods for termination analysis of nondeterministic probabilistic programs with polynomial guards and assignments. Our approach is through synthesis of polynomial ranking supermartingales, that on one hand significantly generalizes linear ranking supermartingales and on the other hand is a counterpart of polynomial ranking-functions for proving termination of nonprobabilistic programs. The approach synthesizes polynomial ranking-supermartingales through Positivstellensatz's, yielding an efficient method which is not only sound, but also semi-complete over a large subclass of programs. We show experimental results to demonstrate that our approach can handle several classical programs with complex polynomial guards and assignments, and can synthesize efficient quadratic ranking-supermartingales when a linear one does not exist even for simple affine programs.
Publishing Year
Date Published
2016-07-01
Volume
9779
Page
3 - 22
Conference
CAV: Computer Aided Verification
Conference Location
Toronto, Canada
Conference Date
2016-07-17 – 2016-07-23
IST-REx-ID

Cite this

Chatterjee K, Fu H, Goharshady A. Termination analysis of probabilistic programs through Positivstellensatz’s. In: Vol 9779. Springer; 2016:3-22. doi:10.1007/978-3-319-41528-4_1
Chatterjee, K., Fu, H., & Goharshady, A. (2016). Termination analysis of probabilistic programs through Positivstellensatz’s (Vol. 9779, pp. 3–22). Presented at the CAV: Computer Aided Verification, Toronto, Canada: Springer. https://doi.org/10.1007/978-3-319-41528-4_1
Chatterjee, Krishnendu, Hongfei Fu, and Amir Goharshady. “Termination Analysis of Probabilistic Programs through Positivstellensatz’s,” 9779:3–22. Springer, 2016. https://doi.org/10.1007/978-3-319-41528-4_1.
K. Chatterjee, H. Fu, and A. Goharshady, “Termination analysis of probabilistic programs through Positivstellensatz’s,” presented at the CAV: Computer Aided Verification, Toronto, Canada, 2016, vol. 9779, pp. 3–22.
Chatterjee K, Fu H, Goharshady A. 2016. Termination analysis of probabilistic programs through Positivstellensatz’s. CAV: Computer Aided Verification, LNCS, vol. 9779. 3–22.
Chatterjee, Krishnendu, et al. Termination Analysis of Probabilistic Programs through Positivstellensatz’s. Vol. 9779, Springer, 2016, pp. 3–22, doi:10.1007/978-3-319-41528-4_1.

Link(s) to Main File(s)
Access Level
OA Open Access

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar