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

TL;DR

This paper investigates the expressivity and computational complexity of TeamLTL, a modal logic capable of expressing hyperproperties, and establishes key decidability and undecidability results for its model checking problems.

Contribution

It relates TeamLTL's expressivity to hyperproperty logics and identifies the boundaries of decidability for model checking in various fragments.

Findings

Decidability of model checking for the left-flat fragment of downward closed TeamLTL extensions.

Undecidability of model checking for TeamLTL with Boolean disjunction and inclusion atoms.

Relation of TeamLTL's expressivity to HyperLTL and HyperQPTL.

Abstract

We study the expressivity and complexity of model checking linear temporal logic with team semantics (TeamLTL). TeamLTL, despite being a purely modal logic, is capable of defining hyperproperties, i.e., properties which relate multiple execution traces. TeamLTL has been introduced quite recently and only few results are known regarding its expressivity and its model checking problem. We relate the expressivity of TeamLTL to logics for hyperproperties obtained by extending LTL with trace and propositional quantifiers (HyperLTL and HyperQPTL). By doing so, we obtain a number of model checking results for TeamLTL and identify its undecidability frontier. In particular, we show decidability of model checking of the so-called left-flat fragment of any downward closed TeamLTL-extension. Moreover, we establish that the model checking problem of TeamLTL with Boolean disjunction and inclusion atoms is undecidable.