Probabilistic Hyperproperties with Rewards

Lukas Wilke, Oyendrila Dobe, Erika Abraham, Ezio Bartocci, Borzoo Bonakdarpour

Probabilistic hyperproperties describe system properties that are concerned with the probability relation between different system executions. Likewise, it is desirable to relate performance metrics (e.g., energy, execution time, etc) between multiple runs. This paper introduces the notion of rewards to the temporal logic HyperPCTL by extending the syntax and semantics of the logic to express the accumulated reward relation among different computations. We demonstrate the application of the extended logic in expressing side-channel timing countermeasures, recovery time in distributed self-stabilizing systems, efficiency in probabilistic conformance, and path planning in robotics applications. We also propose a model checking algorithm for verifying Markov decision processes against HyperPCTL with rewards and report experimental results.