This is a summary of the group meeting on 27 January 2021

Stochastic Invariants for Probabilistic Termination.

In this paper, they address the probabilistic termination problem for linear-arithmetic probabilistic programs with nondeterminism. They extend pure invariants to stochastic invariants and establish the connection between probabilistic termination and linear ranking supermartingale based on stochastic invariants. Also, they propose the concept of replusing supermartingale and use it to analysis probabilistic termination. They also design an algorithm to synthesize a stochastic invariant and compute linear replusing supermartingale.

Q: How to compute a linear repulsing supermartingale? A: Given PI, first we compute the minimal c to make 1-LRepSM exist by LP. Then, in the j-th iteration, we try c+j as difference bound and minimize $\mu_j(l_{init},x_{init})$ to calculate a $\mu_j$ by LP. According to $\mu_j$, we can calculate $p_j$ by Thm. 4.

Q: How large are the examples in the experiment? A: See Sect. 8 in the paper. The probabilistic programs are not very large.