Name
Abstract | ||
|---|---|---|
Probabilistic hyperproperties describe system properties involving probability measures over multiple runs and have numerous applications in information-flow security. However, the poor scalability of existing model checking algorithms for probabilistic hyperproperties limits their use to small models. In this paper, we propose a model checking algorithm to verify discrete-time Markov chains (DTMC) against HyperPCTL formulas by integrating numerical solution techniques. Our algorithm is based on a probabilistic decomposition of the self-composed DTMC into variants of the underlying DTMC. Experimentally, we show that our algorithm significantly outperforms both a symbolic approach and the original approach based on brute-force self-composition. |
Year | DOI | Venue |
|---|---|---|
2022 | 10.1007/978-3-031-07727-2_12 | INTEGRATED FORMAL METHODS, IFM 2022 |
DocType | Volume | ISSN |
Conference | 13274 | 0302-9743 |
Citations | PageRank | References |
0 | 0.34 | 0 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Eshita Zaman | 1 | 0 | 0.34 |
| Gianfranco Ciardo | 2 | 2 | 1.77 |
| Erika Ábrahám | 3 | 830 | 63.17 |
| Borzoo Bonakdarpour | 4 | 490 | 45.02 |