高度增量式：一种面向多目标的简单程序化方法（扩展版）
Highly Incremental: A Simple Programmatic Approach for Many Objectives (Extended Version)
AI总结：
本文提出一种简单程序化方法，通过增量差异分析概率程序的多种目标，如高矩、阈值概率等，利用现有推理方法实现统一分析。
摘要：
我们提出了一种适用于概率程序众多目标的通用程序化方法。首先是在语言中添加奖励语句。然后定义一个程序转换，应用单调函数到程序的累积奖励。关键思想是该转换利用奖励的增量差异。这种简单优雅的方法能够表达例如更高矩、奖励阈值概率、预算超额的期望值以及矩生成函数。所有这些目标现在都可以使用现有的概率wp推理方法进行分析。我们通过Caesar演绎验证器自动化了验证，并报告了该转换在一些示例中的应用。
英文摘要：
We present a one-fits-all programmatic approach to reason about a plethora of objectives on probabilistic programs. The first ingredient is to add a reward-statement to the language. We then define a program transformation applying a monotone function to the cumulative reward of the program. The key idea is that this transformation uses incremental differences in the reward. This simple, elegant approach enables to express e.g., higher moments, threshold probabilities of rewards, the expected excess over a budget, and moment-generating functions. All these objectives can now be analyzed using a single existing approach: probabilistic wp-reasoning. We automated verification using the Caesar deductive verifier and report on the application of the transformation to some examples.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
