On the Expressive Power of TeamLTL and First-Order Team Logic over Hyperproperties
计算机科学中的逻辑
2021-10-22 v1 逻辑
摘要
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ück 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.
引用
@article{arxiv.2110.11109,
title = {On the Expressive Power of TeamLTL and First-Order Team Logic over Hyperproperties},
author = {Juha Kontinen and Max Sandström},
journal= {arXiv preprint arXiv:2110.11109},
year = {2021}
}