Bartocci, E. (2024). Quantifying Uncertainty in Probabilistic Loops Without Sampling: A Fully Automated Approach. In L. Kovacs & A. Sokolova (Eds.), Reachability Problems (pp. 3–8). Springer. https://doi.org/10.1007/978-3-031-72621-7_1
18th International Conference Reachability Problems (RP 2024)
en
Event date:
25-Sep-2024 - 27-Sep-2024
-
Event place:
Wien, Austria
-
Number of Pages:
6
-
Publisher:
Springer
-
Peer reviewed:
Yes
-
Keywords:
Loop Invariants; Analysis of Probabilistic Loop; Statistical Moments
en
Abstract:
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.
en
Project title:
Distribution Recovery for Invariant Generation of Probabilistic Programs: ICT19-018 (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds)
-
Research Areas:
Computer Engineering and Software-Intensive Systems: 100%