HyperProb: A Model Checker for Probabilistic Hyperproperties
HyperProb: A Model Checker for Probabilistic Hyperproperties
复制标题
HyperProb：概率超属性的模型检查器
DOI：
--
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Borzoo Bonakdarpour
中科院分区：
文献类型：
--
作者：
Oyendrila Dobe;E. Ábrahám;E. Bartocci;Borzoo Bonakdarpour
。我们提出了 HyperProb，一个模型检查器，用于验证马尔可夫决策过程 (MDP) 的概率超属性。我们的工具接收表示为 PRISM 模型的 MDP 和超概率计算树逻辑 (HyperPCTL) 中的公式作为输入。通过将调度程序量化的范围限制为无记忆非概率调度程序，我们的工具利用基于 SMT 的编码来对 HyperPCTL 中的概率超属性进行建模。此外，当满足该属性时，该工具可以提供一个见证，可用于合成符合规范的 DTMC。
. 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 formula in Hyper Probabilistic Computational Tree Logic ( HyperPCTL ). 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 provide a witness that can be used for synthesizing a DTMC that conforms with the specification.