HyperProb: A Model Checker for Probabilistic Hyperproperties

Oyendrila Dobe, Erika Abraham, Ezio Bartocci and Borzoo Bonakdarpour

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 HyperPCTL formula. 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 also provide a witness that can be used for synthesizing Markov models that conform with the specification.