Probabilistic Hyperproperties with Nondeterminism

Erika Abraham, Ezio Bartocci, Borzoo Bonakdarpour +1

We study the problem of formalizing and checking probabilistic hyperproperties for models that allow nondeterminism in actions. We extend the temporal logic \HyperPCTL, which has b…