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.

翻译：我们提出了一种精确方法，用于分析和量化含符号参数、多项式运算及潜在不可数状态空间的概率性循环高阶矩的灵敏度。该方法整合了符号计算、概率论与静态分析技术，以自动捕获概率性循环的灵敏度信息。灵敏度信息使我们能够正式建立概率循环变量值分布如何影响循环功能行为，这在选择循环变量值以确保高效/预期计算时尤其有用。本研究利用代数技术，通过线性递推方程对循环变量的高阶矩进行建模，并引入灵敏度递推概念。我们证明，即使当循环变量的矩不满足线性递推系统时，灵敏度递推仍能精确建模循环灵敏度。由此，我们拓展了目前灵敏度分析可适用的概率性循环类别。通过分析概率性循环的灵敏度，我们展示了方法的有效性。