一句话：为随机程序可达概率的上/下近似统一基于鞅的方法，并提出秩上鞅与排斥上鞅两类新技术。
计算可达概率是随机程序分析的基础问题。本文系统梳理并比较基于鞅的方法，用它们对可达概率进行上近似和下近似。作者综合形式验证、控制理论等不同社区的已有工作，给出统一框架，并特别强调序理论不动点这一经典概念在随机程序分析中的作用。该视角进一步催生了两类新的基于鞅的技术，即秩上鞅与排斥上鞅。作者还实现了这些鞅的模板综合算法，并开展实验比较，展示了不同方法的效果与适用性。
Computing reachability probabilities is a fundamental problem in the analysis of randomized programs. This article aims at a comprehensive and comparative account of various martingale-based methods for over- and under-approximating reachability probabilities. Based on the existing works that stretch across different communities (formal verification, control theory, etc.), we offer a unifying account. In particular, we emphasize the role of order-theoretic fixed points—a classic topic in computer science—in the analysis of randomized programs. This leads us to two new martingale-based techniques, too. We also make an experimental comparison using our implementation of template-based synthesis algorithms for those martingales.
@article{paperbot1219,
title = {Ranking and Repulsing Supermartingales for Reachability in Randomized Programs},
author = {Toru Takisaka and Yuichiro Oyabu and Natsuki Urabe and Ichiro Hasuo},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {43},
number = {2},
year = {2021},
doi = {10.1145/3450967}
}