一句话：提出一种表达力充分的定量断言语法，使概率程序基于期望的验证系统达到相对完备。
论文研究概率程序验证中定量断言的语法，即把程序状态映射为数值的函数。作者提出一种表达性语法，并证明其封闭性：若 f 可由该语法表达，则对任意概率程序 C，从初始状态 σ 到 C 终止后最终状态上 f 的期望值，即最弱前置期望 wp[C](f)，也可由该语法表达。由此得到 Cook 意义下相对完备的验证系统：除证明两个语法表达式函数间的不等式外，给定 f、g、C，还可检查 g ≼ wp[C](f)。这为期望值与概率推理提供了统一而表达充分的规约与验证框架。
We study a syntax for specifying quantitative assertions —functions mapping program states to numbers—for probabilistic program verification. We prove that our syntax is expressive in the following sense: Given any probabilistic program C , if a function f is expressible in our syntax, then the function mapping each initial state σ to the expected value of evaluated in the final states reached after termination of C on σ (also called the weakest preexpectation wp[ C ]( f )) is also expressible in our syntax. As a consequence, we obtain a relatively complete verification system for reasoning about expected values and probabilities in the sense of Cook: Apart from proving a single inequality between two functions given by syntactic expressions in our language, given f , g , and C , we can check whether g ≼ wp[ C ]( f ).
@article{paperbot1181,
title = {Relatively complete verification of probabilistic programs: an expressive language for expectation-based reasoning},
author = {Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Christoph Matheja},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434320}
}