Name
Abstract | ||
|---|---|---|
AbstractComputing 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. |
Year | DOI | Venue |
|---|---|---|
2021 | 10.1145/3450967 | ACM Transactions on Programming Languages and Systems |
Keywords | DocType | Volume |
Randomized program, reachability, fixed point, martingale | Journal | 43 |
Issue | ISSN | Citations |
2 | 0164-0925 | 0 |
PageRank | References | Authors |
0.34 | 0 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Toru Takisaka | 1 | 0 | 0.34 |
| Yuichiro Oyabu | 2 | 0 | 0.34 |
| Natsuki Urabe | 3 | 14 | 4.69 |
| Ichiro Hasuo | 4 | 29 | 8.36 |