Linear-time Temporal Logic with Team Semantics: Expressivity and Complexity

We study the expressivity and the model checking problem of linear temporal logic with team semantics (TeamLTL). In contrast to LTL, TeamLTL is capable of defining hyperproperties, i.e., properties which relate multiple execution traces. Logics for hyperproperties have so far been mostly obtained by extending temporal logics like LTL and QPTL with trace quantification, resulting in HyperLTL and HyperQPTL. We study the expressivity of TeamLTL and its extensions in comparison to HyperLTL and HyperQPTL. By doing so we obtain a number of model checking results for TeamLTL and identify its undecidability frontier. The two types of logics follow a fundamentally different approach to hyperproperties and are of incomparable expressivity. We establish that the universally quantified fragment of HyperLTL subsumes the so-called k-coherent fragment of TeamLTL with contradictory negation. This also implies that the model checking problem is decidable for the fragment. We show decidability of model checking of the so-called left-flat fragment of TeamLTL with downward-closed generalised atoms and Boolean disjunction via a translation to a decidable fragment of HyperQPTL. Finally, we show that the model checking problem of TeamLTL with Boolean disjunction and inclusion atoms is undecidable.