In this article we study linear temporal logics with team semantics (TeamLTL) that are novel logics for defining hyperproperties. We define Kamp-type translations of these logics into fragments of first-order team logic and second-order logic. We also characterize the expressive power and the complexity of model-checking and satisfiability of team logic and second-order logic by relating them to second- and third-order arithmetic. Our results set in a larger context the recent results of L\"uck showing that the extension of TeamLTL by the Boolean negation is highly undecidable under the so-called synchronous semantics. We also study stutter-invariant fragments of extensions of TeamLTL.

翻译：在文章中,我们用团队语义学(TeamLTL)来研究线性时间逻辑(TeamLTL),这些逻辑是用来界定超异性的新逻辑。我们将这些逻辑的Kamp型转换成一等团队逻辑和二等逻辑的碎片。我们还通过将团队逻辑和二等逻辑与二等和三等算术联系起来,来描述表达力和模型检查的复杂性和对称性逻辑和二等逻辑。我们的结果在更大的范围内设定了L\"uck"的最新结果,显示TechLTL在所谓的同步语义学下被布尔恩否定的延伸是不可分辨的。我们还研究了TechLT的扩展的细微异性碎片。