将异步性引入概率超属性
Introducing Asynchronicity to Probabilistic Hyperproperties
AI总结：
本文提出 AHyperPCTL，通过量化可随机空转延迟决策的停顿调度器，为概率超逻辑 HyperPCTL 引入执行间异步性，可表达信息流安全策略并给出可判定片段的模型检验算法。
摘要：
概率超属性用于表达具有不确定行为的系统在不同执行之间的概率关系。HyperPCTL 能够将此类属性形式化，其中通过对概率调度器进行量化来解决潜在的非确定性。本文提出名为 AHyperPCTL 的扩展，通过对 stutter-schedulers（停顿调度器）进行量化，在所观察的执行之间额外引入异步性；这类调度器可随机决定通过空转来延迟调度决策。据我们所知，这是概率分支时间超逻辑的首个异步扩展。我们表明 AHyperPCTL 能够表达有意义的信息流安全策略，并针对一个可判定片段提出了模型检验算法。
英文摘要：
Probabilistic hyperproperties express probabilistic relations between different executions of systems with uncertain behavior. HyperPCTL allows to formalize such properties, where quantification over probabilistic schedulers resolves potential non-determinism. In this paper we propose an extension named AHyperPCTL to additionally introduce asynchronicity between the observed executions by quantifying over stutter-schedulers, which may randomly decide to delay scheduler decisions by idling. To our knowledge, this is the first asynchronous extension of a probabilistic branching-time hyperlogic. We show that AHyperPCTL can express interesting information-flow security policies, and propose a model checking algorithm for a decidable fragment.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
