论文标题
异步性超构物的时间逻辑的表现力和可决定性
Expressiveness and Decidability of Temporal Logics for Asynchronous Hyperproperties
论文作者
论文摘要
超专制是将不同执行轨迹的系统的属性，以及从安全性到对称性的许多应用程序，并发的一致性模型等。近年来，已经研究了不同的线性时间逻辑，用于指定异步性超构成。尽管对这些逻辑的模型检查是不可确定的，但已通过应用程序确定了有用的可决定片段。用于异步安全分析。在本文中，我们解决了异步性超代理的时间逻辑的表达性和可决定性问题。我们通过获得几乎完整的表现力图，将这些逻辑的表达与S1S的扩展S1 [E]与等级谓词进行比较。我们还研究了这些逻辑的表达能力，当时在单例痕迹上解释。我们表明，对于HyperLTL的两个异步扩展，检查单例模型的存在已经是不可证实的，对于其中一个模型，即hyperconts hyperltl（hyperltl_c），我们以添加的标准fo [<]的扩展而建立了单例模型的表征。最后的结果概括了fo [<]和ltl之间的众所周知的等效性。最后，我们确定了模型检查hyperltl_c的可决定性的新边界。
Hyperproperties are properties of systems that relate different executions traces, with many applications from security to symmetry, consistency models of concurrency, etc. In recent years, different linear-time logics for specifying asynchronous hyperproperties have been investigated. Though model checking of these logics is undecidable, useful decidable fragments have been identified with applications e.g. for asynchronous security analysis. In this paper, we address expressiveness and decidability issues of temporal logics for asynchronous hyperproperties. We compare the expressiveness of these logics together with the extension S1S[E] of S1S with the equal-level predicate by obtaining an almost complete expressiveness picture. We also study the expressive power of these logics when interpreted on singleton sets of traces. We show that for two asynchronous extensions of HyperLTL, checking the existence of a singleton model is already undecidable, and for one of them, namely Context HyperLTL (HyperLTL_C), we establish a characterization of the singleton models in terms of the extension of standard FO[<] over traces with addition. This last result generalizes the well-known equivalence between FO[<] and LTL. Finally, we identify new boundaries on the decidability of model checking HyperLTL_C.
