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}
}