Automated analysis of probabilistic loops

Abstract

This thesis addresses challenges and advancements in the automated analysis of probabilistic loops. It contributes to the theoretical foundations and computational techniques for analyzing the safety and liveness of probabilistic loops. A core contribution is the development of a fully automated method for computing higher moments of program variables for a large class of probabilistic loops. This method leverages linear recurrences with constant coefficients to model higher moments of loop variables and compute their exact closed-form expressions. Introducing the theory of moment-computable loops, we show that our approach is complete for a class of programs supporting branching statements, polynomial arithmetic, and both discrete and continuous probability distributions. For probabilistic systems with unknown model parameters, we introduce a novel technique for automatic sensitivity analysis with respect to these parameters. By representing unknown parameters with symbolic constants and modeling sensitivities using recurrences, we show that our technique is applicable even to loops that are not moment-computable. Furthermore, this thesis explores hardness bounds for computing the strongest polynomial invariant for classical polynomial loops, showing that this problem SKOLEM-hard. As an intermediary result of independent interest, we show that point-to-point reachability for polynomial dynamical systems is also SKOLEM-hard. Through the notion of moment invariant ideals, we extend these hardness results from classical to probabilistic program analysis. Despite the hardness results, we propose a method for computing polynomial invariants of bounded degree for (probabilistic) polynomial loops and a synthesis procedure to over-approximate polynomial loops with linearizable loops. Additionally, the thesis introduces POLAR, a tool implementing the developed techniques,demonstrating its capability to analyze benchmarks previously out of reach for state-of-the-art methods. Regarding termination analysis, we propose a novel approach based on asymptotic bounds for polynomial probabilistic loops, leading to the development of AMBER, the first tool to certify both probabilistic termination and non-termination.