Quantitative analysis of probabilistic programs aims at deriving tight numerical bounds for probabilistic properties such as expectation and assertion probability, and plays a crucial role in the verification of probabilistic programs. Along this line of research, most existing works consider numerical bounds over the whole state space monolithically and do not consider piecewise bounds. Clearly, monolithic bounds are either conservative, or not expressive and succinct enough in general. To derive more succinct, expressive and precise numerical bounds for probabilistic properties, we propose a novel approach for synthesizing piecewise linear bounds in this work. To this end, we first show how to extract a piecewise feature w.r.t. a given quantitative property from a probabilistic program using latticed $k$-induction that captures a wide and representative class of piecewise bound functions. Second, we develop an algorithmic approach to synthesize piecewise linear upper and lower bounds from the piecewise feature, for which we show that the synthesis of piecewise linear bounds can be reduced to bilinear programming. Third, we implement our approach with the bilinear programming solver Gurobi. The experimental results indicate that our approach is capable of generating tight or even accurate piecewise linear bounds for an extensive set of benchmarks compared with the state of the art.

翻译：概率程序的定量分析旨在推导概率性质（如期望值和断言概率）的紧致数值界，在概率程序验证中发挥着关键作用。现有研究大多整体考虑整个状态空间上的数值界，而未关注分段界。显然，整体界要么过于保守，要么在表达能力和简洁性方面存在不足。为推导更简洁、更具表达力且更精确的概率性质数值界，本文提出一种合成分段线性界的新方法。首先，我们展示了如何通过捕获宽泛且具代表性的分段界函数类的格值$k$-归纳法，从概率程序中提取关于给定定量性质的分段特征。其次，我们开发了一种从分段特征合成分段线性上下界的算法方法，并证明分段线性界的合成可归约为双线性规划问题。最后，我们使用双线性规划求解器Gurobi实现了该方法。实验结果表明，与现有技术相比，该方法能为大量基准测试生成紧致甚至精确的分段线性界。