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.

翻译：我们提出一种精确方法，用于分析和量化具有符号参数、多项式算术及潜在不可数状态空间的概率循环的高阶矩敏感性。该方法融合符号计算、概率论与静态分析的技术，可自动捕捉概率循环的敏感性信息。敏感性信息使我们能够形式化地建立概率循环变量值分布对循环功能行为的影响机制，尤其在通过选择循环变量值确保高效/预期计算时具有重要指导意义。本研究采用代数技术通过线性递推方程建模循环变量的高阶矩，并引入敏感性递推的概念。我们证明，即便在循环变量矩不满足线性递推方程组的情况下，敏感性递推仍能精确建模循环敏感性。据此，我们拓展了迄今可实现敏感性分析的概率循环类别。通过分析概率循环的敏感性，我们验证了该方法的有效性。