We present team semantics for two of the most important linear and branching time specification languages, Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). With team semantics, LTL is able to express hyperproperties, which have in the last decade been identified as a key concept in the verification of information flow properties. We study basic properties of the logic and classify the computational complexity of its satisfiability, path, and model checking problem. Further, we examine how extensions of the basic logic react to adding additional atomic operators. Finally, we compare its expressivity to the one of HyperLTL, another recently introduced logic for hyperproperties. Our results show that LTL with team semantics is a viable alternative to HyperLTL, which complements the expressivity of HyperLTL and has partially better algorithmic properties. For CTL with team semantics, we investigate the computational complexity of the satisfiability and model checking problem. The satisfiability problem is shown to be EXPTIME-complete while we show that model checking is PSPACE-complete.

翻译：我们针对两种最重要的线性和分支时序规范语言——线性时序逻辑（LTL）与计算树逻辑（CTL）——提出了团队语义。借助团队语义，LTL能够表达超属性，这一概念在过去十年中被确立为信息流属性验证中的关键要素。我们研究了该逻辑的基本性质，并对其可满足性、路径及模型检测问题的计算复杂度进行了分类。进一步地，我们探讨了基础逻辑的扩展在引入额外原子运算符时的表现。最后，我们将其表达能力与近期提出的另一种超属性逻辑HyperLTL进行了比较。研究结果表明，具备团队语义的LTL是HyperLTL的一个可行替代方案，它既补充了HyperLTL的表达能力，又在部分算法性质上表现更优。对于具备团队语义的CTL，我们研究了其可满足性与模型检测问题的计算复杂度。可满足性问题被证明是EXPTIME完全的，而模型检测问题则被证明是PSPACE完全的。