On the Expressive Power of TeamLTL and First-Order Team Logic over Hyperproperties

TL;DR

This paper investigates the expressive power and complexity of TeamLTL and first-order team logic for hyperproperties, providing translations, characterizations, and complexity analyses related to second- and third-order arithmetic.

Contribution

It introduces Kamp-type translations of TeamLTL into first-order and second-order team logic, and characterizes their expressive power and complexity, extending understanding of hyperproperty logics.

Findings

TeamLTL can be translated into first-order and second-order team logic fragments.

The expressive power of these logics relates to second- and third-order arithmetic.

Undecidability results are extended to certain logic extensions under synchronous semantics.

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.