Inquisitive Team Semantics of LTL

TL;DR

This paper introduces InqLTL, a new team semantics for LTL inspired by inquisitive logic, which features an intuitionistic implication and Boolean disjunction, and explores its expressiveness and decidability properties.

Contribution

The paper presents InqLTL with a novel team semantics, analyzes its expressive power, and identifies a decidable fragment suitable for hyperproperty specification.

Findings

InqLTL with Boolean negation is highly undecidable.

InqLTL with Boolean negation is less expressive than TeamLTL.

A decidable fragment of InqLTL can express relevant hyperproperties.

Abstract

In this paper, we introduce a novel team semantics of LTL inspired by inquisitive logic. The main features of the resulting logic, we call InqLTL, are the intuitionistic interpretation of implication and the Boolean semantics of disjunction. We show that InqLTL with Boolean negation is highly undecidable and strictly less expressive than TeamLTL with Boolean negation. On the positive side, we identify a meaningful fragment of InqLTL with a decidable model-checking problem which can express relevant classes of hyperproperties. To the best of our knowledge, this fragment represents the first hyper logic with a decidable model-checking problem which allows unrestricted use of temporal modalities and universal second-order quantification over traces.