论文标题
关于线性时间逻辑与团队语义的复杂性
On the Complexity of Linear Temporal Logic with Team Semantics
论文作者
论文摘要
线性时间逻辑（LTL）中给出的公式给出的规范通过其一组跟踪定义系统。但是，某些功能（例如信息流安全约束）相当建模为所谓的超构物，这是一组痕迹。一种合乎逻辑的方法是团队逻辑，这是依赖和独立性规范的逻辑框架。 LTL带有团队语义的LTL最近被发现是超专业的逻辑。我们研究了LTL与所谓同步团队语义和布尔否定的复杂性理论方面，并证明其模型检查和令人满意的问题都是高度无法确定的，相当于三阶算术的决策问题。此外，我们证明这种复杂性已经出现在小时的深度上，并且只有“未来”模态F。最后，我们还引入了团队对结巴不变的概括。
A specification given as a formula in linear temporal logic (LTL) defines a system by its set of traces. However, certain features such as information flow security constraints are rather modeled as so-called hyperproperties, which are sets of sets of traces. One logical approach to this is team logic, which is a logical framework for the specification of dependence and independence of information. LTL with team semantics has recently been discovered as a logic for hyperproperties. We study the complexity theoretic aspects of LTL with so-called synchronous team semantics and Boolean negation, and prove that both its model checking and satisfiability problems are highly undecidable, and equivalent to the decision problem of third-order arithmetic. Furthermore, we prove that this complexity already appears at small temporal depth and with only the "future" modality F. Finally, we also introduce a team-semantical generalization of stutter-invariance.
