[Back]


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.