Talks and Poster Presentations (with Proceedings-Entry):
O. Dobe, E. Abraham, E. Bartocci, B. Bonakdarpour:
"HyperProb: A Model Checker for Probabilistic Hyperproperties";
Talk: FM 2021: the 24th international symposium of Formal Methods,
China;
2021-11-20
- 2021-11-25; in: "Proc. of FM 2021: the 24th international symposium of Formal Methods",
(2021),
657
- 666.
English abstract:
We present HyperProb, a model checker to verify probabilistic hyperproperties on Markov Decision Processes (MDP). Our tool receives as input an MDP expressed as a PRISM model and a formula in Hyper Probabilistic Computational Tree Logic (HyperPCTL). By restricting the domain of scheduler quantification to memoryless non-probabilistic schedulers, our tool exploits an SMT-based encoding to model check probabilistic hyperproperties in HyperPCTL. Furthermore, when the property is satisfied, the tool can provide a witness that can be used for synthesizing a DTMC that conforms with the specification.
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/978-3-030-90870-6_35
Created from the Publication Database of the Vienna University of Technology.