Flavors of Quantifiers in Hyperlogics

TL;DR

This paper extends hypertrace logic by introducing unconstrained trace quantifiers, enabling reasoning over all possible traces in addition to traces fixed by the model, and investigates how different quantifier patterns affect satisfiability.It establishes three key expressiveness results: unconstrained hypertrace logic is expressively equivalent to ${\text{S1S}}$, the trace-prefixed fragment is equivalent to ${\mathsf{HyperQPTL}}$, and mixtures with existential-to-universal constrained quantifier alternations yield decidable fragments, while time-prefix formulations can become undecidable.The central technique is a flattening and translation framework that preserves satisfiability across fragments, enabling reductions between unconstrained hypertrace logic, S1S, HyperQPTL, and HyperQPTL-like traces, as well as reductions from Minsky machine computations to time-prefix formulas to prove undecidability.Overall, the work clarifies how quantifier choice and quantifier placement drive decidability and expressiveness in hyperlogics and lays groundwork for transferring methods between hyperlogics and classical first-order reasoning.

Abstract

Hypertrace logic is a sorted first-order logic with separate sorts for time and execution traces. Its formulas specify hyperproperties, which are properties relating multiple traces. In this work, we extend hypertrace logic by introducing trace quantifiers that range over the set of all possible traces. In this extended logic, formulas can quantify over two kinds of trace variables: constrained trace variables, which range over a fixed set of traces defined by the model, and unconstrained trace variables, which can be assigned to any trace. In comparison, hyperlogics such as HyperLTL have only constrained trace quantifiers. We use hypertrace logic to study how different quantifier patterns affect the decidability of the satisfiability problem. We prove that hypertrace logic without constrained trace quantifiers is equivalent to monadic second-order logic of one successor (S1S), and therefore satisfiable, and that the trace-prefixed fragment (all trace quantifiers precede all time quantifiers) is equivalent to HyperQPTL. Moreover, we show that all hypertrace formulas where the only alternation between constrained trace quantifiers is from an existential to a universal quantifier are equisatisfiable to formulas without constraints on their trace variables and, therefore, decidable as well. Our framework allows us to study also time-prefixed hyperlogics, for which we provide new decidability and undecidability results

Theorems & Definitions (22)

• Theorem 1: S1SBuchi60
• Theorem 2: Kamp1968gabbay1980temporal
• Example 3
• Example 4
• Lemma 5
• Corollary 6
• Theorem 7
• Corollary 8
• Lemma 9
• Example 10