Quantifying Uncertainty in Probabilistic Loops Without Sampling: A Fully Automated Approach

A probabilistic loop is a programming control flow structure whose behavior depends on random variables’ assignments and probabilistic conditions. One challenging problem is quantifying automatically the uncertainty of the probabilistic loop behavior for a potentially unbounded number of iterations. Although this problem is generally highly undecidable, we have explored the necessary restrictions enabling the automated analysis of probabilistic loops without user intervention. Our symbolic approach leverages algebraic methods and the statistical properties of well-defined probability distributions to derive closed-form expressions of the higher-order statistical moments for the program’s random variables at each loop iteration. In this talk, we demonstrate the application of our methodology through a series of examples.