论文标题
带有团队语义的线性时间逻辑：表现力和复杂性
Linear-time Temporal Logic with Team Semantics: Expressivity and Complexity
论文作者
论文摘要
我们研究使用团队语义（TeamLTL）的模型检查线性时间逻辑的表达和复杂性。尽管纯粹是模态逻辑，但TeamLTL能够定义超专业，即与多个执行跟踪相关的属性。 TeamLTL最近是最近引入的，关于其表达性及其模型检查问题的结果很少。我们将TeamLTL与逻辑的表达性联系起来，用于通过用痕量和命题量化器（HyperLTL和HyperQPTL）扩展LTL获得的超普罗代理。通过这样做，我们获得了TeamLTL的许多模型检查结果，并确定其不可证明的前沿。特别是，我们显示了任何向下封闭的TeamLTL扩展的所谓的左翼片段的模型检查的可决定性。此外，我们确定具有布尔分离和包容原子的TeamLTL的模型检查问题是不可确定的。
We study the expressivity and complexity of model checking linear temporal logic with team semantics (TeamLTL). TeamLTL, despite being a purely modal logic, is capable of defining hyperproperties, i.e., properties which relate multiple execution traces. TeamLTL has been introduced quite recently and only few results are known regarding its expressivity and its model checking problem. We relate the expressivity of TeamLTL to logics for hyperproperties obtained by extending LTL with trace and propositional quantifiers (HyperLTL and HyperQPTL). By doing so, we obtain a number of model checking results for TeamLTL and identify its undecidability frontier. In particular, we show decidability of model checking of the so-called left-flat fragment of any downward closed TeamLTL-extension. Moreover, we establish that the model checking problem of TeamLTL with Boolean disjunction and inclusion atoms is undecidable.
