概率程序的多目标预期望推理
Multiobjective Preexpectation Reasoning for Probabilistic Programs
AI总结：
针对带非确定性的概率程序规划问题，提出多目标预期望变换器及对应策略综合规则，构建了无限MDP上多目标优化的程序层面符号方法。
AI中文摘要：
带非确定性的概率程序可对规划问题建模，其中策略会消解非确定性以优化期望结果。我们研究多目标场景，即沿帕累托前沿同时优化多个结果，并提供策略综合的演绎式程序层面说明。其核心是多目标预期望变换器，它将后期望元组映射到同时可达值的集合，该集合属于凸Hoare幂域。它保守扩展了最弱预期望并提升了标准循环规则。我们开发规则以综合见证策略，作为在非概率确定性上随机化的混合确定性。我们证明该变换器和综合规则针对操作型MDP语义是可靠的，且不要求有限状态空间：我们的方法可视为针对无限MDP上多目标优化的程序层面符号方法。我们通过多个案例研究展示了我们的机制。
英文摘要：
Probabilistic programs with nondeterminism model planning problems in which a strategy resolves the nondeterminism to optimize an expected outcome. We study the multiobjective setting, optimizing several outcomes at once along a Pareto front, and provide a deductive, program-level account of strategy synthesis. Its core is a multiobjective preexpectation transformer mapping a tuple of postexpectations to the set of simultaneously achievable values, an element of the convex Hoare powerdomain. It conservatively extends weakest preexpectations and lifts standard loop rules. We develop rules to synthesize witnessing strategies as mixed determinizations that randomize over non-probabilistic determinizations. We prove the transformer and synthesis rules sound against an operational MDP semantics, without requiring a finite state space: our approach can be seen as a symbolic approach - at program level - for multiobjective optimization over infinite MDPs. We demonstrate our machinery using various case studies.
