On the Expressive Power of TeamLTL and First-Order Team Logic over Hyperproperties
Logic in Computer Science
2021-10-22 v1 Logic
Abstract
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.
Keywords
Cite
@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}
}