一句话：首次提出异步超属性的自动机模型与不动点演算 Hµ，并给出可判定近似分析。
超属性在安全分析等领域日益重要，但既有方法多聚焦同步分析，即按锁步比较不同路径。本文系统研究异步超属性分析，提出交替异步奇偶自动机（Alternating Asynchronous Parity Automata）与时间不动点演算 Hµ；后者是首个能系统表达异步超属性并包含已有逻辑 HyperLTL 的不动点演算。作者证明在固定路径指派下，两种模型的表达力一致。二者表达力极强，导致相关决策问题高度不可判定，甚至不在算术层级内。为此，论文提出近似分析方法，并由此得到自然的可判定片段。
Hyperproperties have received increasing attention in the last decade due to their importance e.g. for security analyses. Past approaches have focussed on synchronous analyses, i.e. techniques in which different paths are compared lockstepwise. In this paper, we systematically study asynchronous analyses for hyperproperties by introducing both a novel automata model (Alternating Asynchronous Parity Automata) and the temporal fixpoint calculus H µ , the first fixpoint calculus that can systematically express hyperproperties in an asynchronous manner and at the same time subsumes the existing logic HyperLTL. We show that the expressive power of both models coincides over fixed path assignments. The high expressive power of both models is evidenced by the fact that decision problems of interest are highly undecidable, i.e. not even arithmetical. As a remedy, we propose approximative analyses for both models that also induce natural decidable fragments.
@article{paperbot1193,
title = {Automata and fixpoints for asynchronous hyperproperties},
author = {Jens Oliver Gutsfeld and Markus Müller-Olm and Christoph Ohrem},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434319}
}