Ranking and Repulsing Supermartingales for Reachability in Probabilistic Programs

TL;DR

This paper provides a comprehensive comparison of martingale-based methods for estimating reachability probabilities in probabilistic programs, introduces two new techniques, and validates them through rigorous proofs and experiments.

Contribution

It unifies various martingale-based approaches across disciplines and introduces two novel methods with proven soundness and completeness.

Findings

New martingale techniques with rigorous proofs

Experimental comparison of synthesis algorithms

Unified framework for reachability analysis

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.