Ranking and Repulsing Supermartingales for Reachability in Probabilistic Programs
Abstract
Computing reachability probabilities is a fundamental problem in the analysis of probabilistic programs. This paper aims at a comprehensive and comparative account on 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 probabilistic programs. This leads us to two new martingale-based techniques, too. We give rigorous proofs for their soundness and completeness. We also make an experimental comparison using our implementation of template-based synthesis algorithms for those martingales.
Cite
@article{arxiv.1805.10749,
title = {Ranking and Repulsing Supermartingales for Reachability in Probabilistic Programs},
author = {Toru Takisaka and Yuichiro Oyabu and Natsuki Urabe and Ichiro Hasuo},
journal= {arXiv preprint arXiv:1805.10749},
year = {2018}
}