Abstract
We present an exact approach to analyze and quantify the sensitivity of higher moments of probabilistic loops with symbolic parameters, polynomial arithmetic and potentially uncountable state spaces. Our approach integrates methods from symbolic computation, probability theory, and static analysis in order to automatically capture sensitivity information about probabilistic loops. Sensitivity information allows us to formally establish how value distributions of probabilistic loop variables influence the functional behavior of loops, which can in particular be helpful when choosing values of loop variables in order to ensure efficient/expected computations. Our work uses algebraic techniques to model higher moments of loop variables via linear recurrence equations and introduce the notion of sensitivity recurrences. We show that sensitivity recurrences precisely model loop sensitivities, even in cases where the moments of loop variables do not satisfy a system of linear recurrences. As such, we enlarge the class of probabilistic loops for which sensitivity analysis was so far feasible. We demonstrate the success of our approach while analyzing the sensitivities of probabilistic loops.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
While [27] allows arbitrary dependencies among finite valued variables, our work omits this generalization for simplicity. Nevertheless, our results also apply to admissible loops with arbitrary dependencies among finite valued variables.
References
Aguirre, A., Barthe, G., Hsu, J., Kaminski, B.L., Katoen, J., Matheja, C.: A pre-expectation calculus for probabilistic sensitivity. In: Proceedings of the POPL (2021). https://doi.org/10.1145/3434333
Amrollahi, D., Bartocci, E., Kenison, G., Kovács, L., Moosbrugger, M., Stankovic, M.: Solving invariant generation for unsolvable loops. In: Proceedings of the SAS (2022). https://doi.org/10.1007/978-3-031-22308-2_3
Barthe, G., Espitau, T., Ferrer Fioriti, L.M., Hsu, J.: Synthesizing probabilistic invariants via Doob’s decomposition. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 43–61. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41528-4_3
Barthe, G., Espitau, T., Grégoire, B., Hsu, J., Strub, P.: Proving expected sensitivity of probabilistic programs. In: Proceedings of the POPL (2018). https://doi.org/10.1145/3158145
Barthe, G., Grégoire, B., Zanella Béguelin, S.: Probabilistic relational Hoare logics for computer-aided security proofs. In: Gibbons, J., Nogueira, P. (eds.) MPC 2012. LNCS, vol. 7342, pp. 1–6. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31113-0_1
Barthe, G., Katoen, J.P., Silva, A.: Foundations of Probabilistic Programming. Cambridge University Press (2020). https://doi.org/10.1017/9781108770750
Barthe, G., Köpf, B., Olmedo, F., Béguelin, S.Z.: Probabilistic relational reasoning for differential privacy. In: Proceedings of the POPL (2012). https://doi.org/10.1145/2103656.2103670
Bartocci, E., Kovács, L., Stankovič, M.: Automatic generation of moment-based invariants for prob-solvable loops. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 255–276. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-31784-3_15
Bartocci, E., Kovács, L., Stankovič, M.: Analysis of Bayesian networks via prob-solvable loops. In: Pun, V.K.I., Stolz, V., Simao, A. (eds.) ICTAC 2020. LNCS, vol. 12545, pp. 221–241. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-64276-1_12
Bartocci, E., Kovács, L., Stankovič, M.: Mora - automatic generation of moment-based invariants. In: TACAS 2020. LNCS, vol. 12078, pp. 492–498. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45190-5_28
Breck, J., Cyphert, J., Kincaid, Z., Reps, T.W.: Templates and recurrences: better together. In: Proceedings of the PLDI (2020). https://doi.org/10.1145/3385412.3386035
Chakarov, A., Sankaranarayanan, S.: Expectation invariants for probabilistic program loops as fixed points. In: Müller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 85–100. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10936-7_6
Chan, H., Darwiche, A.: When do numbers really matter? J. Artif. Intell. Res. (2002). https://doi.org/10.1613/jair.967
Chan, H., Darwiche, A.: Sensitivity analysis in Bayesian networks: from single to multiple parameters. In: Proceedings of the UAI (2004)
Chou, Y., Yoon, H., Sankaranarayanan, S.: Predictive runtime monitoring of vehicle models using Bayesian estimation and reachability analysis. In: Proceedings of the IROS (2020). https://doi.org/10.1109/IROS45743.2020.9340755
Durrett, R.: Probability: Theory and Examples. Cambridge University Press (2019). https://doi.org/10.1017/9781108591034
Everest, G., van der Poorten, A., Shparlinski, I., Ward, T.: Recurrence Sequences. Mathematical Surveys and Monographs, vol. 104. American Mathematical Society, Providence, RI (2003)
Farzan, A., Kincaid, Z.: Compositional recurrence analysis. In: Proceedings of the FMCAD (2015)
Ghahramani, Z.: Probabilistic machine learning and artificial intelligence. Nature (2015). https://doi.org/10.1038/nature14541
Gretz, F., Katoen, J.-P., McIver, A.: Prinsys—on a quest for probabilistic loop invariants. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 193–208. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40196-1_17
Huang, Z., Wang, Z., Misailovic, S.: PSense: automatic sensitivity analysis for probabilistic programs. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 387–403. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-01090-4_23
Humenberger, A., Jaroschek, M., Kovács, L.: Invariant generation for multi-path loops with polynomial assignments. In: VMCAI 2018. LNCS, vol. 10747, pp. 226–246. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-73721-8_11
Kauers, M., Paule, P.: The Concrete Tetrahedron. Symbolic Sums, Recurrence Equations, Generating Functions, Asymptotic Estimates. Springer, Vienna (2011). https://doi.org/10.1007/978-3-7091-0445-3
Kincaid, Z., Cyphert, J., Breck, J., Reps, T.W.: Non-linear reasoning for invariant synthesis. In: Proceedings of the POPL (2018). https://doi.org/10.1145/3158142
Kovács, L.: Reasoning algebraically about P-solvable loops. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 249–264. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_18
Moosbrugger, M., Müllner, J., Kovács, L.: Automated sensitivity analysis for probabilistic loops (2023). https://arxiv.org/abs/2305.15259
Moosbrugger, M., Stankovic, M., Bartocci, E., Kovács, L.: This is the moment for probabilistic loops. In: Proceedings of the ACM on Programming Languages (OOPSLA2) (2022). https://doi.org/10.1145/3563341
Motwani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press (1995). https://doi.org/10.1017/cbo9780511814075
Rodríguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial loop invariants: algebraic foundations. In: Gutierrez, J. (ed.) Proceedings of the ISSAC (2004). https://doi.org/10.1145/1005285.1005324
Rodríguez-Carbonell, E., Kapur, D.: Generating all polynomial invariants in simple loops. J. Symb. Comput. (2007). https://doi.org/10.1016/j.jsc.2007.01.002
Selyunin, K., Ratasich, D., Bartocci, E., Islam, M.A., Smolka, S.A., Grosu, R.: Neural programming: towards adaptive control in cyber-physical systems. In: Proceedings of the CDC (2015). https://doi.org/10.1109/CDC.2015.7403319
Stankovic, M., Bartocci, E., Kovács, L.: Moment-based analysis of Bayesian network properties. Theor. Comput. Sci. (2022). https://doi.org/10.1016/j.tcs.2021.12.021
Vasilenko, E., Vazou, N., Barthe, G.: Safe couplings: coupled refinement types. In: Proceedings of the ICFP (2022). https://doi.org/10.1145/3547643
Wang, P., Fu, H., Chatterjee, K., Deng, Y., Xu, M.: Proving expected sensitivity of probabilistic programs with randomized variable-dependent termination time. In: Proceedings of the POPL (2020). https://doi.org/10.1145/3371093
Acknowledgements
This research was supported by the Vienna Science and Technology Fund WWTF 10.47379/ICT19018 grant ProbInG, the ERC Consolidator Grant ARTIST 101002685, the Austrian FWF SFB project SpyCoDe F8504, and the SecInt Doctoral College funded by TU Wien.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Moosbrugger, M., Müllner, J., Kovács, L. (2024). Automated Sensitivity Analysis for Probabilistic Loops. In: Herber, P., Wijs, A. (eds) Integrated Formal Methods. iFM 2023. Lecture Notes in Computer Science, vol 14300. Springer, Cham. https://doi.org/10.1007/978-3-031-47705-8_2
Download citation
DOI: https://doi.org/10.1007/978-3-031-47705-8_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-47704-1
Online ISBN: 978-3-031-47705-8
eBook Packages: Computer ScienceComputer Science (R0)