Paper Info
Title
Ranking and Repulsing Supermartingales for Approximating Reachability.
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.
Year
Venue
Field
2018
arXiv: Programming Languages
Martingale (probability theory),Ranking,Computer science,Theoretical computer science,Reachability,Mathematical proof,Soundness,Probabilistic logic,Completeness (statistics),Formal verification
DocType
Volume
Citations 
Journal
abs/1805.10749
0
PageRank 
References 
Authors
0.34
0
4
Name
Order
Citations
PageRank
Toru Takisaka101.35
Yuichiro Oyabu200.34
Natsuki Urabe3144.69
Ichiro Hasuo4101.90