Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Inquisitive Team Semantics of LTL

Laura Bozzelli, Tadeusz Litak, Munyque Mittelmann, Aniello Murano

TL;DR

InqLTL presents a team-semantics extension of LTL inspired by inquisitive logic, using intuitionistic implication and Boolean disjunction to express hyperproperties over sets of traces. While InqLTL({\sim}) is highly undecidable (via reductions from second-order arithmetic), a meaningful left-positive fragment is decidable for model checking, aided by macro-path semantics and an automata-theoretic approach using Hesitant Alternating Word Automata. The paper shows InqLTL is strictly weaker than TeamLTL({\sim}) in expressiveness, but its left-positive fragment supports rich properties, including information-flow constraints and universal subteam quantification. The abstraction via macro-paths and the automata construction provide a significant step toward practical verification of hyperproperties with unrestricted temporal modalities and universal second-order quantification over traces, suggesting broad avenues for future work on complexity, asynchronous variants, and branching-time extensions.

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.

Inquisitive Team Semantics of LTL

TL;DR

InqLTL presents a team-semantics extension of LTL inspired by inquisitive logic, using intuitionistic implication and Boolean disjunction to express hyperproperties over sets of traces. While InqLTL({\sim}) is highly undecidable (via reductions from second-order arithmetic), a meaningful left-positive fragment is decidable for model checking, aided by macro-path semantics and an automata-theoretic approach using Hesitant Alternating Word Automata. The paper shows InqLTL is strictly weaker than TeamLTL({\sim}) in expressiveness, but its left-positive fragment supports rich properties, including information-flow constraints and universal subteam quantification. The abstraction via macro-paths and the automata construction provide a significant step toward practical verification of hyperproperties with unrestricted temporal modalities and universal second-order quantification over traces, suggesting broad avenues for future work on complexity, asynchronous variants, and branching-time extensions.

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.
Paper Structure (29 sections, 28 theorems, 43 equations, 1 figure)

This paper contains 29 sections, 28 theorems, 43 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Our contribution.
  3. Preliminaries
  4. Kripke Structures.
  5. $\text{\sffamily TeamLTL}$.
  6. Inquisitive $\text{\sffamily LTL}$
  7. Expressiveness issues.
  8. Examples of specifications
  9. Undecidability of $\text{\sffamily InqLTL}({\sim})$
  10. Encoding of variable valuations.
  11. Decidability results
  12. Macro-path semantics for $\text{\sffamily InqLTL}$
  13. Macro-path semantics.
  14. Model checking of left-positive $\text{\sffamily InqLTL}$
  15. Translation into $\text{\sffamily HAA}$.
  16. ...and 14 more sections

Key Result

Proposition 1

$\text{\sffamily InqLTL}$ formulas satisfy downward closure, empty, and singleton equivalence properties. Hence, $\text{\sffamily InqLTL}$ satisfiability reduces to $\text{\sffamily LTL}$ satisfiability. Moreover, for all $\text{\sffamily InqLTL}({\sim})$ formulas $\varphi$ and teams $\mathcal{L}$,

Figures (1)

  • Figure 1: Encoding of a cell of a $k$-grid for $k=2$

Theorems & Definitions (41)

  • Proposition 1
  • Example 1
  • Proposition 2: Countable Model Property
  • Proposition 3
  • proof
  • Proposition 4
  • Proposition 5
  • Proposition 6
  • proof : Sketched proof.
  • Proposition 7
  • ...and 31 more