Probabilistic Hyperproperties with Rewards
Probabilistic Hyperproperties with Rewards
复制标题
有奖励的概率超属性
DOI：
--
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Borzoo Bonakdarpour
中科院分区：
文献类型：
--
作者：
Oyendrila Dobe;Lukas Wilke;E. Ábrahám;E. Bartocci;Borzoo Bonakdarpour
.概率超性质描述的是与不同系统执行之间的概率关系有关的系统性质。同样，期望将性能度量（例如，能量、执行时间等）。本文通过扩展时态逻辑HyperPCTL的语法和语义，将奖励的概念引入到时态逻辑HyperPCTL中，使之能够表示不同计算之间的累积奖励关系。我们展示了扩展逻辑在表达侧信道定时对策，概率一致性的效率，机器人应用中的路径规划，以及分布式自稳定系统中的恢复时间中的应用。我们还提出了一个模型检测算法，用于验证马尔可夫决策过程对HyperPCTL的奖励和报告的实验结果。
. Probabilistic hyperproperties describe system properties that are concerned with the probability relation between different system ex-ecutions. 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, efficiency 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.
DOI：
10.1109/csf51468.2021.00009
发表时间：
2021
期刊：
2021 IEEE 34th Computer Security Foundations Symposium (CSF
影响因子：
--
作者：
Wang, Yu;Nalluri, Siddhartha;Bonakdarpour, Borzoo;Pajic, Miroslav
通讯作者：
Pajic, Miroslav