用于异步超属性的自动机与不动点

超属性在过去十年中因其对安全分析等方面的重要性而受到越来越多的关注。以往的方法侧重于同步分析，即在不同路径之间以锁步方式进行比较的技术。在本文中，我们通过引入一种新颖的自动机模型（交替异步奇偶自动机）以及时序不动点演算 $\Hmu$，系统地研究了超属性的异步分析；$\Hmu$ 是首个能够以异步方式系统地表达超属性，同时又能涵盖现有逻辑 HyperLTL 的不动点演算。我们证明了这两种模型在固定路径赋值上的表达能力是一致的。两种模型的高表达能力体现在相关决策问题是高度不可判定的，即甚至不属于算术层级。作为补救，我们为这两种模型提出了近似分析，其也诱导出自然的可判定片段。