一句话：重新审视时序团队语义，提出三种量化时间求值函数的异步 hyperproperty 逻辑，并分析其可判定性。
论文重新考察时序团队语义的基础，以处理异步 hyperproperties。作者定义三种逻辑，它们通过加入对所谓时间求值函数（time evaluation functions）的量化来控制迹的异步推进。论文把同步逻辑嵌入新逻辑，并证明带布尔析取的相关逻辑的模型检测问题高度不可判定，证明方法为编码非确定性 2-counter 机的循环计算。最后，作者给出到交替异步 Büchi 自动机的翻译，得到路径检测问题的可判定性，以及受限模型检测与可满足性问题的可判定性。该工作把异步 hyperproperties 的逻辑刻画与自动机方法联系起来。
In this paper, we study a novel approach to asynchronous hyperproperties by reconsidering the foundations of temporal team semantics. We consider three logics: , and , which are obtained by adding quantification over so-called time evaluation functions controlling the asynchronous progress of traces. We then relate synchronous to our new logics and show how it can be embedded into them. We show that the model checking problem for with Boolean disjunctions is highly undecidable by encoding recurrent computations of non-deterministic 2-counter machines. Finally, we present a translation from to Alternating Asynchronous Büchi Automata and obtain decidability results for the path checking problem as well as restricted variants of the model checking and satisfiability problems.