Termination Analysis of Probabilistic Programs through\n Positivstellensatz's

We consider nondeterministic probabilistic programs with the most basic\nliveness property of termination. We present efficient methods for termination\nanalysis of nondeterministic probabilistic programs with polynomial guards and\nassignments. Our approach is through synthesis of polynomial ranking\nsupermartingales, that on one hand significantly generalizes linear ranking\nsupermartingales and on the other hand is a counterpart of polynomial\nranking-functions for proving termination of nonprobabilistic programs. The\napproach synthesizes polynomial ranking-supermartingales through\nPositivstellensatz's, yielding an efficient method which is not only sound, but\nalso semi-complete over a large subclass of programs. We show experimental\nresults to demonstrate that our approach can handle several classical programs\nwith complex polynomial guards and assignments, and can synthesize efficient\nquadratic ranking-supermartingales when a linear one does not exist even for\nsimple affine programs.\n