一句话：提出基于最弱前置条件的演绎框架，半自动地为含随机与纯非确定的命令式程序合成无记忆确定性策略，使其满足期望界等定量规约。
论文研究同时包含随机性与纯非确定性的命令式程序：核心问题是找到一个消解纯非确定的策略，使得确定化后的程序满足给定的定量规约，例如程序变量最终期望值的界或终止于某状态集合的概率界。作者提出一种半自动的演绎验证方法，以最弱前置条件风格框架构造无记忆且确定（MD）的策略；对无循环程序，所得策略的正确性由构造保证；对带循环程序，则需为循环提供合适的循环不变式，与程序验证中的做法类似。论文还说明该技术与可数无限马尔可夫决策过程里 reachability-reward 目标下获取策略这一经典问题的联系，并通过若干案例研究展示方法的适用性。
We consider imperative programs that involve both randomization and pure nondeterminism. The central question is how to find a strategy resolving the pure nondeterminism such that the so-obtained determinized program satisfies a given quantitative specification, i.e., bounds on expected outcomes such as the expected final value of a program variable or the probability to terminate in a given set of states. We show how memoryless and deterministic (MD) strategies can be obtained in a semi-automatic fashion using deductive verification techniques. For loop-free programs, the MD strategies resulting from our weakest preconditionstyle framework are correct by construction. This extends to loopy programs, provided the loops are equipped with suitable loop invariants - just like in program verification. We show how our technique relates to the well-studied problem of obtaining strategies in countably infinite Markov decision processes with reachabilityreward objectives. Finally, we apply our technique to several case studies.
@article{paperbot2585,
title = {Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs},
author = {Kevin Batz and Tom Jannik Biskup and Joost-Pieter Katoen and Tobias Winkler},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632935}
}