HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties
HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties
复制标题
DOI：
10.1007/978-3-319-99154-2_2
复制
发表时间：
2018-04
期刊：
影响因子：
--
通讯作者：
E. Ábrahám;Borzoo Bonakdarpour
中科院分区：
文献类型：
--
作者：
E. Ábrahám;Borzoo Bonakdarpour
本文提出了一种新的时态逻辑来表示和推理概率超性质.超性质描述了系统中不同独立执行之间的关系，概率超性质描述了这些执行之间的定量依赖关系.概率系统的标准时态逻辑，即，PCTLandPCTL一次只能引用一条路径，因此不能表达许多感兴趣的概率超性质。本文提出的逻辑，HyperPCTL，增加了明确的和同时量化多个跟踪到PCTL。这种量化允许表达概率超性质。离散时间马尔可夫链的模型检测算法的建议的逻辑也被引入。
In this paper, we propose a new temporal logic for expressing and reasoning about probabilistic hyperproperties.Hyperpropertiescharacterize the relation between different independent executions of a system.Probabilistichyperproperties express quantitative dependencies between such executions. The standard temporal logics for probabilistic systems, i.e.,PCTLandPCTLcan refer only to a single path at a time and, hence, cannot express many probabilistic hyperproperties of interest. The logic proposed in this paper,HyperPCTL, adds explicit and simultaneous quantification over multiple traces toPCTL. Such quantification allows expressing probabilistic hyperproperties. A model checking algorithm for the proposed logic is also introduced for discrete-time Markov chains.