Publication Type
Year of Publication
2022
Conference/Journal Name
NASA Formal Methods Symposium
Page Numbers
656-673
Abstract
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 di erent computations. We demonstrate the application of the extended logic in expressing side-channel timing countermeasures, effciency in probabilistic conformance, path planning in robotics applications, and recovery time in distributed self-stabilizing systems. We also propose a model checking algorithm for verifying Markov Decision Processes against HyperPCTL with rewards and report experimental results.
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 di erent computations. We demonstrate the application of the extended logic in expressing side-channel timing countermeasures, effciency in probabilistic conformance, path planning in robotics applications, and recovery time in distributed self-stabilizing systems. We also propose a model checking algorithm for verifying Markov Decision Processes against HyperPCTL with rewards and report experimental results.
