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.

BibTeX Citation

@InProceedings{10.1007/978-3-030-90870-6_35,
author="Dobe, Oyendrila
and {\'A}brah{\'a}m, Erika
and Bartocci, Ezio
and Bonakdarpour, Borzoo",
editor="Huisman, Marieke
and P{\u{a}}s{\u{a}}reanu, Corina
and Zhan, Naijun",
title="HyperProb: A Model Checker for Probabilistic Hyperproperties",
booktitle="Formal Methods",
year="2021",
publisher="Springer International Publishing",
address="Cham",
pages="657--666",
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.",
isbn="978-3-030-90870-6"
}