Stankovic, M., & Bartocci, E. (2024). Probabilistic Loop Synthesis from Sequences of Moments. In J. Hillston, S. Soudjani, & M. Waga (Eds.), Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems (pp. 233–248). https://doi.org/10.1007/978-3-031-68416-6_14
Quantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems (QEST+FORMATS 2024)
en
Event date:
9-Sep-2024 - 13-Sep-2024
-
Event place:
Canada
-
Number of Pages:
16
-
Peer reviewed:
Yes
-
Keywords:
Probabilistic Programs; Program synthesis
en
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.
-
Project title:
Distribution Recovery for Invariant Generation of Probabilistic Programs: ICT19-018 (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds) Training and Guiding AI Agents with Ethical Rules: ICT22-023 (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds)
-
Research Areas:
Computer Engineering and Software-Intensive Systems: 100%
