Termination analysis of probabilistic programs through Positivstellensatz's Conference Paper

Author(s): Chatterjee, Krishnendu; Fu, Hongfei; Goharshady, Amir K
Title: Termination analysis of probabilistic programs through Positivstellensatz's
Title Series: LNCS
Affiliation IST Austria
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.
Keywords: Computer aided analysis; Probabilistic programs; Complex polynomials; Liveness properties; Non-probabilistic; Positivstellensatz; Ranking functions; Supermartingales; Termination analysis
Conference Title: CAV: Computer Aided Verification
Volume: 9779
Conference Dates: July 17-23, 2016
Conference Location: Toronto, Canada
Publisher: Springer  
Date Published: 2016-07-01
Start Page: 3
End Page: 22
DOI: 10.1007/978-3-319-41528-4_1
Notes: We thank anonymous referees for valuable comments. We also thank Hui Kong for his help on SOSTOOLS. The research was partly supported by Austrian Science Fund (FWF) NFN Grant No. S11407-N23 (RiSE/SHiNE), ERC Start grant (279307: Graph Games), ERC Advanced Grant (267989: QUAREM), and Natural Science Foundation of China (NSFC) under Grant No. 61532019.
Open access: yes (repository)
IST Austria Authors
  1. Hongfei Fu
    2 Fu
Related IST Austria Work