Kofnov, A., Moosbrugger, M., Stankovič, M., Bartocci, E., & Bura, E. (2022). Moment-Based Invariants for Probabilistic Loops with Non-polynomial Assignments. In E. Ábrahám & M. Paolieri (Eds.), Quantitative Evaluation of Systems (pp. 3–25). Springer. https://doi.org/10.1007/978-3-031-16336-4_1
E105-08 - Forschungsbereich Angewandte Statistik E192-04 - Forschungsbereich Formal Methods in Systems Engineering E191-01 - Forschungsbereich Cyber-Physical Systems
We present a method to automatically approximate moment-based invariants of probabilistic programs with non-polynomial updates of continuous state variables to accommodate more complex dynamics. Our approach leverages polynomial chaos expansion to approximate non-linear functional updates as sums of orthogonal polynomials. We exploit this result to automatically estimate state-variable moments of all orders in Prob-solvable loops with non-polynomial updates. We showcase the accuracy of our estimation approach in several examples, such as the turning vehicle model and the Taylor rule in monetary policy.
en
Project title:
Distribution Recovery for Invariant Generation of Probabilistic Programs: ICT19-018 (WWTF Wiener Wissenschafts-, Forschu und Technologiefonds) Prognostizierung einer suffizienten Dimensions-Reduktions-Methodik: P 30690-N35 (Fonds zur Förderung der wissenschaftlichen Forschung (FWF)) Automated Reasoning with Theories and Induction for Software Technologies: ERC Consolidator Grant 2020 / 101002685 (European Commission)
-
Research Areas:
Logic and Computation: 30% Mathematical and Algorithmic Foundations: 40% Computer Engineering and Software-Intensive Systems: 30%
