Probabilistic Loop Synthesis from Sequences of Moments

Abstract

Probabilistic program synthesis consists in automatically creating programs generating random values adhering to specified distributions. We consider here the family of probabilistic programs with a potentially non-terminating loop and with linear updates drawing from iteration-independent univariate distributions. We develop an algorithm to synthesise a probabilistic loop given as property the closed-form expressions of the first three statistical moments in the number of loop iterations. Our approach supports random draws from Gaussian, discrete, or a combination of discrete and continuous distributions. We illustrate the effectiveness of our method through various examples.