论文标题
马尔可夫决策过程的概率超专制
Probabilistic Hyperproperties of Markov Decision Processes
论文作者
论文摘要
超专制是将系统的正确性描述为多个执行之间的关系的属性。 HyperProperties概括了跟踪属性，并包括信息流的安全要求，例如非干预，以及对称性，部分观察，稳健性和容错的要求。我们启动了马尔可夫决策过程（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.
