标题： 超逻辑中的量词类型 显示英文标题

标题： Flavors of Quantifiers in Hyperlogics

摘要： 超轨迹逻辑是一种带有时间与执行轨迹单独排序的一阶逻辑。其公式指定超性质，这些性质是涉及多个轨迹的性质。在本工作中，我们通过引入范围涵盖所有可能轨迹集合的轨迹量词来扩展超轨迹逻辑。在该扩展逻辑中，公式可以对两种类型的轨迹变量进行量化：受限轨迹变量，其范围是模型中定义的固定轨迹集合；以及非受限轨迹变量，可以分配到任何轨迹。相比之下，如HyperLTL这样的超逻辑仅包含受限轨迹量词。我们使用超轨迹逻辑来研究不同的量词模式如何影响可满足性问题的可判定性。我们证明，没有受限轨迹量词的超轨迹逻辑等价于一个后继的单二阶逻辑（S1S），因此是可满足的，并且轨迹前缀片段（所有轨迹量词都位于所有时间量词之前）等价于HyperQPTL。此外，我们表明，所有仅在受限轨迹量词之间存在从存在量词到全称量词的交替的超轨迹公式，与没有轨迹变量约束的公式是等可满足的，因此也是可判定的。我们的框架还允许我们研究时间前缀超逻辑，并为此提供了新的可判定性和不可判定性结果。 显示英文摘要

摘要： 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