Probabilistic Hyperproperties of Markov Decision Processes
Probabilistic Hyperproperties of Markov Decision Processes
复制标题
马尔可夫决策过程的概率超性质
DOI：
--
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Hazem Torfah
中科院分区：
文献类型：
--
作者：
Rayna Dimitrova;B. Finkbeiner;Hazem Torfah
超属性是将系统正确性描述为多次执行之间关系的属性。超属性概括了跟踪属性，包括信息流安全要求（例如互不干扰）以及对称性、部分观察、鲁棒性和容错性等要求。我们启动了马尔可夫决策过程（MDP）超性质的规范和验证的研究。我们引入了时序逻辑 PHL（概率超逻辑），它通过对调度程序和跟踪的量化来扩展经典概率逻辑。 PHL 可以表达概率系统的广泛超属性，包括概率无干扰等经典应用，以及机器人和规划等领域的新颖应用。虽然 PHL 的模型检查问题通常是不可判定的，但我们提供了从逻辑片段证明和反驳公式的方法。该片段包括许多感兴趣的概率超性质。
Hyperproperties are properties that describe the correctness of a system as a relation between multiple executions. Hyperproperties generalize trace properties and include information-flow security requirements, like noninterference, as well as requirements like symmetry, partial observation, robustness, and fault tolerance. We initiate the study of the specification and verification of hyperproperties of Markov decision processes (MDPs). We introduce the temporal logic PHL (Probabilistic Hyper Logic), which extends classic probabilistic logics with quantification over schedulers and traces. PHL can express a wide range of hyperproperties for probabilistic systems, including both classical applications, such as probabilistic noninterference, and novel applications in areas such as robotics and planning. While the model checking problem for PHL is in general undecidable, we provide methods both for proving and for refuting formulas from a fragment of the logic. The fragment includes many probabilistic hyperproperties of interest.