Temporal logics have been studied as an approach to the specification of hyperproperties, resulting in the conception of "hyperlogics". With a few recent exceptions, the hyperlogics thus far developed can only relate different traces of a transition system synchronously. However, important information is contained in the relation between different points in their asynchronous interaction. To specify such "asynchronous hyperproperties", new trace quantifier based hyperlogics have been developed. Yet, hyperlogics with trace quantification cannot express certain requirements that describe the relationships between all executions of a system. Also, these logics induce model checking problems (MC) with prohibitively high complexity costs in the number of quantifier alternations. We study an alternative approach to asynchronous hyperproperties by introducing a novel foundation of temporal team semantics. Team semantics is a logical framework that specifies properties of sets of traces of unbounded size directly, and thus does not have the same limitation as the quantifier based logics mentioned above. We consider temporal team logics which employ quantification over so-called "time evaluation functions" (TEFs) controlling the asynchronous progress of traces instead of quantification over traces. TEFs constitute a novel approach to defining expressive logics for hyperproperties where diverse asynchronous interactions between computations can be formalised and enforced. We show embeddings of synchronous TeamLTL into our new logics. We show that MC for some TeamCTL fragment is highly undecidable. We present a translation from TeamCTL* to Alternating Asynchronous B\"uchi Automata, and obtain decidability results for the path checking problem and restrictions of MC and SAT. Our translation constitutes the first approach to team semantics based on automata-theoretic methods.

翻译：时序逻辑已被研究作为超属性规范的一种方法，从而催生了"超逻辑"的概念。除少数近期例外，迄今为止发展的超逻辑只能同步关联迁移系统的不同轨迹。然而，异步交互中不同时刻之间的关系包含重要信息。为规范此类"异步超属性"，基于轨迹量化的新型超逻辑已被提出。但基于轨迹量化的超逻辑无法表达描述系统所有执行之间关系的某些需求。此外，这些逻辑引发的模型检测问题在量词交替次数上具有极高的复杂度。我们通过引入时序团队语义的新基础，研究了一种异步超属性的替代方法。团队语义是一种直接规范任意大小轨迹集合属性的逻辑框架，因此不具备上述基于量词逻辑的相同局限性。我们考虑用时序团队逻辑，它使用对所谓"时间评估函数"（TEFs）的量词代替对轨迹的量词，以控制轨迹的异步演进。TEFs构成定义超属性表达性逻辑的新方法，其中可形式化并强制执行计算间多样的异步交互。我们展示了同步TeamLTL到新逻辑的嵌入。我们证明某些TeamCTL片段的模型检测问题是高度不可判定的。我们提出从TeamCTL*到交替异步Büchi自动机的转化，并获得了路径检测问题以及模型检测和可满足性限制的可判定性结果。我们的转化构成了基于自动机理论的团队语义方法的首次尝试。