2025-11-15T14:52:11.063010

Flavors of Quantifiers in Hyperlogics

Chalupa, Henzinger, da Costa

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

academic

Flavors of Quantifiers in Hyperlogics

基本信息

论文ID: 2510.12298
标题: Flavors of Quantifiers in Hyperlogics
作者: Marek Chalupa, Thomas A. Henzinger, Ana Oliveira da Costa (IST Austria)
分类: cs.LO (Logic in Computer Science), cs.FL (Formal Languages)
发表会议: FSTTCS 2025 (45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science)
论文链接: https://arxiv.org/abs/2510.12298

超性质的表达需求：传统的时间逻辑(如LTL)只能推理单个执行轨迹，无法表达涉及比较多个执行的超性质(hyperproperties)，如信息流安全、一致性等。
现有超逻辑的限制：现有的超逻辑(如HyperLTL)只有受约束的轨迹量词，即只能在给定系统的轨迹集合上量化，这限制了其表达能力。
可判定性问题：超逻辑的可满足性问题通常是不可判定的，需要找到具有可判定可满足性的片段。

研究动机

本文的核心动机是通过引入无约束轨迹量词来增强超轨迹逻辑的表达能力，同时系统性地研究不同量词模式对可判定性的影响。这种扩展允许在所有可能轨迹的宇宙上量化，而不仅仅是系统的轨迹集合。

核心贡献

扩展超轨迹逻辑：引入了无约束轨迹量词，使得公式可以在所有可能轨迹上量化，显著增强了表达能力。
建立等价性关系：
- 证明无约束超轨迹逻辑等价于S1S
- 证明轨迹前缀超轨迹逻辑等价于HyperQPTL
可判定性结果：识别了具有可判定可满足性问题的新片段，特别是受约束量词交替模式为∃*∀*的片段。
时间前缀片段分析：首次系统性地研究了时间量词优先的超逻辑片段，提供了新的可判定性和不可判定性结果。

φ ::= ∃π φ | ∃π::T φ | ∃i φ | ¬φ | φ ∨ φ | i < i | i = i | X(π,i)

其中：

∃π φ：无约束轨迹量词
∃π::T φ：受约束轨迹量词
∃i φ：时间量词
X(π,i)：二元谓词，表示轨迹π在时间i的性质

语义定义

公式在轨迹集合T上的满足关系通过标准一阶逻辑语义定义：

无约束量词：(T,(ΠT,ΠN)) ⊨ ∃π φ 当且仅当存在τ ∈ (2^X)^ω使得(T,(ΠT[π↦τ],ΠN)) ⊨ φ
受约束量词：(T,(ΠT,ΠN)) ⊨ ∃π::T φ 当且仅当存在τ ∈ T使得(T,(ΠT[π↦τ],ΠN)) ⊨ φ

技术创新点

1. Flatten函数

引入flatten函数来重写超轨迹公式，利用无约束轨迹变量中变量赋值的独立性：

flatten(∃π φ, {x₀,...,xₙ}, Vc) = ∃πx₀...∃πxₙ flatten(φ, {x₀,...,xₙ}, Vc∪{π})

关键洞察：无约束轨迹变量的不同命题变量可以独立量化，这为建立与S1S的等价性奠定基础。

2. 与S1S的等价性证明

通过以下翻译建立无约束超轨迹逻辑与S1S的双向等价性：

从超轨迹到S1S：

使用flatten重写公式
将每个πx重新解释为二阶变量
替换σ = {x(πx,i) ↦ πx(i)}

从S1S到超轨迹：

每个二阶变量X变成轨迹变量τX
使用标准的Succ到≤的翻译

3. 受约束量词的消除技术

对于量词模式为∃::T ∀::T的公式，提供消除全称受约束量词的方法：

通过将全称量词展开为所有现有存在轨迹变量的组合：

∀π₁::T...∀πₘ::T φ ≡ ⋀ⱼ₁₌₁ⁿ...⋀ⱼₘ₌₁ⁿ φ[π₁↦πⱼ₁,...,πₘ↦πⱼₘ]

实验设置

理论验证方法

本文主要是理论工作，通过严格的数学证明验证结果：

构造性证明：通过显式构造翻译函数证明等价性
归纳证明：使用结构归纳证明翻译的正确性
归约证明：通过从已知不可判定问题的归约证明不可判定性

可判定性分析框架

建立了系统性的分析框架：

轨迹前缀片段：所有轨迹量词在时间量词之前
时间前缀片段：所有时间量词在轨迹量词之前
量词交替模式：分析不同的∃和∀交替模式

定理7：无约束超轨迹逻辑与S1S表达能力等价
定理20：轨迹前缀超轨迹逻辑与HyperQPTL等价

2. 可判定性结果汇总

片段	量词模式	可判定性	参考
轨迹前缀	∃T(∃T::T)（∀T::T)QTQ*N<	可判定	推论16
轨迹前缀	(∀T::T)²∃T::TQ+N<	不可判定	命题15
时间前缀	∃N<∃T(∃T::T)*（∀T::T)QT	可判定	推论21
时间前缀	∃N<∀N<∃²N<∀N<∀T::T(∃T::T)²∃T	不可判定	定理22