论文标题
非确定性
Probabilistic Hyperproperties with Nondeterminism
论文作者
论文摘要
我们研究了对允许行动中无确定性的模型进行形式化和检查概率超代理的问题。我们扩展了以前针对离散时间马尔可夫链引入的时间逻辑\ HyperPCTL，以实现Markov决策过程的超专业规范。我们通过对调度程序和概率计算树进行明确和同时量化来概括HyperPCTL，并表明它可以在安全性和隐私中表达重要的定量要求。我们表明，对MDP进行的HyperPCTL模型通常无法确定使用内存的概率调度程序，但是将域限制为无内存的非稳态调度程序，使模型检查问题可确定。随后，我们提出了一个基于SMT的编码，用于检查该语言并评估其性能。
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 been previously introduced for discrete-time Markov chains, to enable the specification of hyperproperties also for Markov decision processes. We generalize HyperPCTL by allowing explicit and simultaneous quantification over schedulers and probabilistic computation trees and show that it can express important quantitative requirements in security and privacy. We show that HyperPCTL model checking over MDPs is in general undecidable for quantification over probabilistic schedulers with memory, but restricting the domain to memoryless non-probabilistic schedulers turns the model checking problem decidable. Subsequently, we propose an SMT-based encoding for model checking this language and evaluate its performance.
