Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A Remark on the Expressivity of Asynchronous TeamLTL and HyperLTL

Juha Kontinen, Max Sandström, Jonni Virtema

TL;DR

The paper investigates the expressivity relations between asynchronous, set-based TeamLTL extensions and HyperLTL. By focusing on modest extensions—TeamLTL with Boolean disjunction and a left-downward closed fragment with Boolean negation—the authors establish precise correspondences to fragments of HyperLTL with a single universal quantifier and its Boolean closures. Specifically, TeamLTL^l(⊕) is equi-expressive with the positive Boolean closure of the one-universal HyperLTL, while left-dc--TeamLTL^l(∼) aligns with the Boolean closure of the one-universal HyperLTL. These results enable transferring decidability properties between the logics and deepen the understanding of how asynchronous team semantics relate to hyperlogics in expressing hyperproperties.

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.

A Remark on the Expressivity of Asynchronous TeamLTL and HyperLTL

TL;DR

The paper investigates the expressivity relations between asynchronous, set-based TeamLTL extensions and HyperLTL. By focusing on modest extensions—TeamLTL with Boolean disjunction and a left-downward closed fragment with Boolean negation—the authors establish precise correspondences to fragments of HyperLTL with a single universal quantifier and its Boolean closures. Specifically, TeamLTL^l(⊕) is equi-expressive with the positive Boolean closure of the one-universal HyperLTL, while left-dc--TeamLTL^l(∼) aligns with the Boolean closure of the one-universal HyperLTL. These results enable transferring decidability properties between the logics and deepen the understanding of how asynchronous team semantics relate to hyperlogics in expressing hyperproperties.

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.
Paper Structure (4 sections, 6 theorems, 17 equations)

This paper contains 4 sections, 6 theorems, 17 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Correspondence between $\mathrm{TeamLTL}\xspace$ and $\mathrm{HyperLTL}$
  4. Conclusion

Key Result

proposition thmcounterproposition

$\mathrm{TeamLTL}\xspace^l$ has both the flatness and the downward closure properties, while $\mathrm{TeamLTL}\xspace^l(\varovee)$ only has the downward closure property.

Theorems & Definitions (17)

  • definition thmcounterdefinition: $\mathrm{TeamLTL}\xspace$
  • proposition thmcounterproposition
  • definition thmcounterdefinition: Syntax of $\mathrm{HyperLTL}$
  • definition thmcounterdefinition: Semantics of $\mathrm{HyperLTL}$
  • definition thmcounterdefinition: Universal Fragments
  • definition thmcounterdefinition: (Positive) Boolean Closure
  • proposition thmcounterproposition
  • proof
  • remark thmcounterremark
  • proposition thmcounterproposition
  • ...and 7 more