Automata and fixpoints for asynchronous hyperproperties
Automata and fixpoints for asynchronous hyperproperties
复制标题
异步超属性的自动机和固定点
DOI：
--
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Christoph Ohrem
中科院分区：
文献类型：
--
作者：
J. Gutsfeld;M. Müller;Christoph Ohrem
由于超属性在安全分析等方面的重要性，超属性在过去十年中受到越来越多的关注。过去的方法都集中在同步分析，即技术，其中不同的路径进行比较锁定逐步。本文通过引入一种新的自动机模型（Alternating Asynchronous Parity Automata）和时间不动点演算Hµ，系统地研究了超性质的异步分析. 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.