Termination Analysis of Probabilistic Programs through Positivstellensatz's

Krishnendu Chatterjee, Hongfei Fu, Amir Kafshdar Goharshady

We consider nondeterministic probabilistic programs with the most basic liveness property of termination. We present efficient methods for termination analysis of nondeterministic…