论文标题
异步性超腐烂的自动机和固定点
Automata and Fixpoints for Asynchronous Hyperproperties
论文作者
论文摘要
由于其重要性，在过去的十年中，超专制受到了越来越多的关注。用于安全分析。过去的方法集中在同步分析上，即比较不同路径的技术。在本文中，我们通过引入一种新型自动机模型（交替的异步均等自动机）和时间fixpoint cyculus $ \ hmu $来系统地研究异步分析，以实现超普业，这是第一个可以系统地表达超级遗物的fixpoint $ \ hmu $，并且在同一时间符合了同一时间的逻辑。我们表明，这两种模型的表达能力都在固定路径分配上重合。两种模型的高表达能力都证明了感兴趣的决策问题是高度无法确定的，即甚至没有算术。作为一种补救措施，我们提出了这两个模型的近似分析，这些模型也诱发了自然的片段。
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 $\Hmu$, 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.
