Open for all UnRAVeL-members: Joost-Pieter Katoen: MOVES Seminar Automated Termination Analysis of Polynomial Probabilistic Programs

Thursday, August 06, 2020, 10:00am

Location: Online Session

Speaker: Joost-Pieter Katoen



In this talk, I will present a fully automated approach to the termination analysis of probabilistic while-programs whose guards and expressions are polynomial expressions. As proving (positive) AST is undecidable in general, existing proof rules typically provide sufficient conditions. These conditions mostly involve constraints on super-martingales. We consider four proof rules from the literature and extend these with generalizations of existing proof rules for (P)AST.

We automate the resulting set of proof rules by effectively computing asymptotic bounds on polynomials over the program variables. These bounds are used to decide the sufficient conditions -- including the constraints on super-martingales -- of a proof rule.

Our approach can thus check AST, PAST, as well as their negations for a large class of polynomial probabilistic programs. Experimental results show the merits of our generalized proof rules and demonstrate that our work can handle probabilistic programs that are out of reach for other state-of-the-art tools.

(Joint work with Ezio Bartocci, Marcel Moosbrugger and Laura Kovacs).