Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
O. Dobe, E. Abraham, E. Bartocci, B. Bonakdarpour:
"HyperProb: A Model Checker for Probabilistic Hyperproperties";
Vortrag: FM 2021: the 24th international symposium of Formal Methods,
China;
20.11.2021
- 25.11.2021; in: "Proc. of FM 2021: the 24th international symposium of Formal Methods",
(2021),
S. 657
- 666.
Kurzfassung englisch:
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.
"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/978-3-030-90870-6_35