Name
Abstract | ||
|---|---|---|
Computing reachability probabilities is a fundamental problem in the analysis of probabilistic programs. This paper aims at a comprehensive and comparative account of various martingale-based methods for over- and underapproximating 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 also make an experimental comparison using our implementation of template-based synthesis algorithms for those martingales. |
Year | DOI | Venue |
|---|---|---|
2018 | 10.1007/978-3-030-01090-4_28 | ATVA |
Field | DocType | ISSN |
Martingale (probability theory),Ranking,Computer science,Theoretical computer science,Reachability,Probabilistic logic,Formal verification | Conference | Automated Technology for Verification and Analysis. ATVA 2018.
Lecture Notes in Computer Science, vol 11138. Springer, Cham |
Citations | PageRank | References |
2 | 0.37 | 15 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Toru Takisaka | 1 | 2 | 0.37 |
| Yuichiro Oyabu | 2 | 2 | 0.37 |
| Natsuki Urabe | 3 | 14 | 4.69 |
| Ichiro Hasuo | 4 | 10 | 1.90 |