A Remark on the Expressivity of Asynchronous TeamLTL and HyperLTL

TL;DR

This paper investigates the expressive power of asynchronous TeamLTL with set-based team semantics and compares it to HyperLTL, revealing equivalences under certain extensions and restrictions.

Contribution

It establishes formal expressiveness equivalences between extended versions of TeamLTL and HyperLTL with restricted quantifiers.

Findings

TeamLTL with disjunction matches positive Boolean closure of HyperLTL with one universal quantifier.

Negation-restricted TeamLTL is expressively equivalent to Boolean closure of HyperLTL with one universal quantifier.

The results clarify the relationship between team semantics and hyperproperties in temporal logics.

Abstract

Linear temporal logic (LTL) is used in system verification to write formal specifications for reactive systems. However, some relevant properties, e.g. non-inference in information flow security, cannot be expressed in LTL. A class of such properties that has recently received ample attention is known as hyperproperties. There are two major streams in the research regarding capturing hyperproperties, namely hyperlogics, which extend LTL with trace quantifiers (HyperLTL), and logics that employ team semantics, extending truth to sets of traces. In this article we explore the relation between asynchronous LTL under set-based team semantics (TeamLTL) and HyperLTL. In particular we consider the extensions of TeamLTL with the Boolean disjunction and a fragment of the extension of TeamLTL with the Boolean negation, where the negation cannot occur in the left-hand side of the Until-operator or within the Global-operator. We show that TeamLTL extended with the Boolean disjunction is equi-expressive with the positive Boolean closure of HyperLTL restricted to one universal quantifier, while the left-downward closed fragment of TeamLTL extended with the Boolean negation is expressively equivalent with the Boolean closure of HyperLTL restricted to one universal quantifier.