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.

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