概率程序的结构抽象与精炼

《Proceedings of the ACM on Programming Languages》：Structural Abstraction and Refinement for Probabilistic Programs

本文提出结构抽象精化框架，将概率控制流自动机转化为马尔可夫决策过程，利用最大可达性作为结构上界，分离概率与计算语义，并构建通用反例引导的抽象精化（CEGAR）框架，结合跟踪抽象实现非随机验证技术的概率程序验证，实验表明其灵活高效。

　　

摘要

在本文中，我们提出了一种名为“结构抽象细化”的新框架，用于验证概率程序的阈值问题。我们的方法通过抽象掉语句的语义，将概率控制流自动机（PCFA）的结构表示为马尔可夫决策过程（MDP）。MDP的“最大可达性”自然地为违规概率提供了一个适当的上限，这个上限被称为“结构上限”。这种方法为PCFA和MDP之间的关系提供了一种新的“结构化”描述，与传统的“语义化”视角形成对比——在传统视角中，MDP反映了程序的语义。该方法的独特之处在于它清晰地分离了概率与计算语义之间的关注点：抽象层仅关注概率计算，而细化层仅处理语义方面；因此，无需修改即可使用非随机程序验证技术。

基于这一特点，我们提出了一个通用的基于反例的抽象细化（CEGAR）框架，该框架能够利用现有的非概率技术来进行概率验证。我们通过跟踪抽象（trace abstraction）对其进行了实例化研究。我们的方法在一系列不同的示例上与最先进的工具进行了对比测试，实验结果展示了其灵活性以及快速处理更复杂结构的能力。