A Temporal Logic for Asynchronous Hyperproperties
A Temporal Logic for Asynchronous Hyperproperties
复制标题
异步超属性的时态逻辑
DOI：
--
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
César Sánchez
中科院分区：
文献类型：
--
作者：
Jan Baumeister;Norine Coenen;Borzoo Bonakdarpour;B. Finkbeiner;César Sánchez
超属性是需要多个跟踪来评估的计算系统的属性，例如许多信息流安全性和并发性要求。跟踪属性定义一组跟踪，而超属性定义一组跟踪集。时态逻辑 HyperLTL 和 HyperCTL* 已被提出来表达超属性。然而，它们的语义是同步的，因为所有跟踪都以相同的速度进行并在相同的位置进行评估。这就排除了使用这些逻辑来分析其迹线可以以不同速度进行的系统，并允许不同的迹线独立地采取断断续续的步骤。为了在本文中解决这个问题，我们提出了 HyperLTL 的异步变体。从消极的一面来看，我们表明该变体的模型检查问题是不可判定的。从积极的一面来看，我们确定了一个可判定的片段，其中涵盖了一组丰富的具有实际应用的公式。我们还提出了两种模型检查算法，将我们的问题简化为同步语义中的 HyperLTL 模型检查问题。
Hyperproperties are properties of computational systems that require more than one trace to evaluate, e.g., many information-flow security and concurrency requirements. Where a trace property defines a set of traces, a hyperproperty defines a set of sets of traces. The temporal logics HyperLTL and HyperCTL* have been proposed to express hyperproperties. However, their semantics are synchronous in the sense that all traces proceed at the same speed and are evaluated at the same position. This precludes the use of these logics to analyze systems whose traces can proceed at different speeds and allow that different traces take stuttering steps independently. To solve this problem in this paper, we propose an asynchronous variant of HyperLTL. On the negative side, we show that the model-checking problem for this variant is undecidable. On the positive side, we identify a decidable fragment which covers a rich set of formulas with practical applications. We also propose two model-checking algorithms that reduce our problem to the HyperLTL model-checking problem in the synchronous semantics.