Model Checking Quantitative Hyperproperties
超性质是计算迹集的性质。在本文中，我们研究了定量超性质，我们定义为超性质，表示在一定的关系可能出现的迹的数量上的界限。例如，定量非干扰限制了通过系统的可观察输出泄露的关于某些秘密输入的信息量。因此，定量非干扰限制了具有相同可观察输入但不同可观察输出的迹线的数量。我们研究的设置HyperLTL，超性质的时间逻辑的定量超性质。我们表明，虽然定量超性能可以表示在HyperLTL，运行时间的HyperLTL模型检验算法是，根据属性的类型，指数，甚至双指数的定量界。我们改进了这种复杂性与一个新的模型检验算法的基础上模型计数。新算法只需要对数空间的界限，因此，根据属性，指数甚至双指数超过模型检验算法的HyperLTL。在最坏的情况下，新算法需要多项式空间的系统的大小。我们的最大#SAT为基础的原型实现表明，然而，计数方法是可行的系统与非平凡的定量信息流的要求，如密码检查。
2019-05-31 cs.LO
The Complexity of Generalized HyperLTL with Stuttering and Contexts
Aalborg University（奥尔堡大学）
本文确定了带 stuttering 和 contexts 的广义 HyperLTL 的可满足性与模型检测复杂度，证明可满足性为 $Σ_1^1$-完全，而模型检测等价于二阶算术真值且远难于 HyperLTL。
2025-09-17 cs.FL cs.LO
The Complexity of Asynchronous HyperLTL
Aalborg University（奥尔堡大学）
本文研究了异步超属性逻辑AHLTL的模型检测和可满足性问题，证明了模型检测等价于二阶算术真值，而可满足性在轨迹存在量化时为Σ₁¹-完全，在轨迹全称量化时为Σ₁¹-困难且属于Σ₂¹。
2026-10-11 cs.LO
Tracy, Traces, and Transducers: Computable Counterexamples and Explanations for HyperLTL Model-Checking
针对HyperLTL模型检测仅提供二元结果的问题，提出基于Skolem函数的两种反例与解释范式，分别实现完备性（限最终周期轨迹）和通用性（图灵机可计算函数），并证明相关可判定性且能计算转换器。
2024-11-26 cs.FL cs.LO
Expressiveness and Decidability of Temporal Logics for Asynchronous Hyperproperties
Hyperproperties是系统的属性，涉及不同的执行轨迹，从安全到对称，并发性的一致性模型等许多应用程序，近年来，不同的线性时间逻辑指定异步hyperproperties进行了研究。虽然这些逻辑的模型检验是不可判定的，但是已经识别出有用的可判定片段，例如用于异步安全分析的应用。在本文中，我们解决异步超性质的时序逻辑的表达性和可判定性问题。我们比较了这些逻辑的表达性，以及S1S的扩展S1S[E]与等级别谓词，通过获得几乎完整的表达性图片。我们还研究了这些逻辑的表达能力时，解释单例集的痕迹。我们表明，对于HyperLTL的两个异步扩展，检查单例模型的存在性已经是不可判定的，对于其中之一，即上下文HyperLTL（HyperLTL_C），我们建立了一个表征的单例模型的扩展标准FO[<]的痕迹与添加。这最后一个结果推广了FO[<]和LTL之间众所周知的等价性。最后，我们确定了新的界限的可判定性的模型检验HyperLTL_C。
2022-07-06 cs.LO
Verifying Hyperliveness
HyperLTL是线性时间时态逻辑的扩展，用于规范超属性，即，与多个计算轨迹相关的时间属性。HyperLTL可以表达信息流策略以及互斥算法中的对称性或抗错误传输协议中的汉明距离等属性。以前的工作对HyperLTL模型检验的重点是替代自由片段的HyperLTL，其中验证减少到检查一个标准的跟踪属性在一个适当的自我组成的系统。然而，无替代片段并不涵盖一般的超活性属性。例如，通用公式不能表达保密要求，即对于秘密变量的每一个可能值，都存在一个计算，其中值是不同的，而外部观察者所做的观察是相同的。在本文中，我们研究了更困难的情况下，hyperliveness属性表示为HyperLTL公式与量词交替。我们减少存在量化的战略选择，并表明合成算法可以用来消除存在量词自动。我们还表明，这种方法可以扩展到反应系统的合成，即，自动构建一个反应系统，保证满足给定的HyperLTL公式。
2020-05-15 cs.LO
The Complexity of Second-order HyperLTL
Bar-Ilan University（巴伊兰大学）；Aalborg University（奥尔堡大学）
本文研究了第二阶超LTL的可满足性、有限状态可满足性及模型检查问题，发现其复杂性等价于三阶算术的真实性。同时分析了两种第二阶超LTL的片段，探讨了其在限制量化范围后的复杂性变化。
2026-03-13 cs.FL cs.LO
A Temporal Logic for Asynchronous Hyperproperties
超性质是计算系统的性质，其需要多于一个迹来评估，例如，许多信息流安全性和并发性要求。在跟踪属性定义一组跟踪的情况下，超属性定义一组多组跟踪。时态逻辑HyperLTL和HyperCTL* 已经被提出来表达超属性。然而，它们的语义是同步的，因为所有跟踪都以相同的速度进行，并在相同的位置进行评估。这就排除了使用这些逻辑来分析其轨迹可以以不同速度进行的系统，并允许不同的轨迹独立地采取断续步骤。为了解决这个问题，在本文中，我们提出了一个异步变体的HyperLTL。在消极的一面，我们表明，这种变体的模型检查问题是不可判定的。在积极的一面，我们确定了一个可判定的片段，其中涵盖了丰富的公式与实际应用。我们还提出了两个模型检测算法，减少我们的问题的同步语义的HyperLTL模型检测问题。
2021-04-28 cs.LO
On Verifying Timed Hyperproperties
我们研究的可满足性和模型检测问题的时间超属性指定的HyperMTL，HyperLTL的时间扩展。根据是否允许在不同的跟踪中交错事件，可以为定时超属性定义两种可能的语义：异步和同步。虽然可满足性问题可以决定类似于HyperLTL的语义的选择，我们表明，模型检查问题，除非规格是替代自由，是不可判定的，即使在非常有限的时间限制是允许的。在积极的一面，我们表明，模型检验HyperMTL与量词交替是可能的，在一定条件下的同步语义，或当有一个固定的时间域的长度上的界限。
2018-12-25 cs.LO
Checking Satisfiability of Hyperproperties using First-Order Logic
CISPA Helmholtz Center for Information Security（CISPA亥姆霍兹信息安全中心）
本文提出FOLHyper工具，通过将超属性问题转化为一阶逻辑公式，实现对超属性可满足性的自动检查，扩展了HyperLTL的分析范围。
2025-12-29 cs.LO
A Temporal Logic of Security
提出了一种新的安全策略验证逻辑。该逻辑HyperLTL扩展了线性时间时态逻辑（LTL），并在多个执行路径上使用连接词进行显式和同时量化，从而使HyperLTL能够表达LTL无法表达的信息流安全策略。给出了一个HyperLTL片段的模型检测算法，并在原型模型检测器中实现了该算法。在HyperLTL中可表达的安全策略类的特征在于超属性的算术层次结构。
2013-07-09 cs.CR cs.LO
Synchronous Team Semantics for Temporal Logics
University of Tübingen（蒂宾根大学）；Institut für Theoretische Informatik, Leibniz Universität Hannover（汉诺威莱布尼茨大学理论计算机科学研究所）；School of Computing Science, University of Glasgow（格拉斯哥大学计算科学学院）；Department of Computer Science, Aalborg University（奥尔堡大学计算机系）
本文为LTL和CTL提出团队语义，使其能表达超性质，研究其计算复杂度并证明带有团队语义的LTL是HyperLTL的可行替代方案。
2026-10-06 cs.LO
Prophecies all the Way: Game-based Model-Checking for HyperQPTL beyond $\forall^*\exists^*$
本文将基于博弈的模型检测方法从$\forall^*\forall^*$片段扩展至支持任意量词前缀的完整HyperQPTL，采用不完全信息博弈实现，同时得到带前瞻转换器的Skolem函数有限状态实现以解释性质满足情况。
2025-07-31 cs.FL cs.LO
Reasoning about Quality in Hyperproperties
Universität Leipzig（莱比锡大学）；Aix Marseille Univ, CNRS, LIS（艾克斯-马赛大学，法国国家科学研究中心，信息系统实验室）；Univ. Bordeaux, CNRS, Bordeaux INP, LaBRI, UMR 5800（波尔多大学，法国国家科学研究中心，波尔多理工学院，计算机研究实验室）
本文提出在HyperLTL中引入定性推理，通过量化属性的满足程度来改进超属性的验证方法。
2026-10-12 cs.LO
Model Checking Algorithms for Hyperproperties
超性质通过表达多个计算之间的关系来推广迹性质。Hyperproperties包括信息流安全策略，如观察确定性或非干扰性，以及许多其他系统属性，包括不确定性和知识。本文综述了时态超逻辑的模型检验问题。我们的出发点是HyperLTL的模型检验算法，这是对Büchi自动机空性的简化。这个基本构造可以用命题量化来扩展，从而产生HyperQPTL的算法。它还可以随着分支时间的延长而扩展，从而形成HyperCTL* 算法。但是，不可能同时拥有两个扩展：HyperQCTL* 的模型检验问题是不可判定的。MPL[E]提供了一个有吸引力的折衷方案，即，一元路径逻辑用等层谓词扩展。MPL[E]的表现力严格介于HyperCTL* 和HyperQCTL* 之间。MPL[E]包含HyperCTL* 和HyperKCTL*，HyperCTL* 的扩展与知识运算符。我们证明了MPL[E]的模型检验问题仍然是可判定的。
2021-07-25 cs.LO
Team Semantics for the Specification and Verification of Hyperproperties
我们开发团队语义的线性时序逻辑（LTL）来表达hyperproperties，这是最近被确定为一个关键的概念，在信息流属性的验证。从概念上讲，我们认为一个异步和同步的团队语义的变体。我们研究了这种新逻辑的基本性质，并对其可满足性、路径和模型检验问题的计算复杂性进行了分类。此外，我们将研究这些基本逻辑的扩展如何对添加其他原子运算符做出反应。最后，我们比较它的表现力的HyperLTL，另一个最近推出的逻辑hyperproperties。我们的研究结果表明，团队语义下的LTL是一个可行的替代HyperLTL，它补充了HyperLTL的表达能力，并具有部分更好的算法性能。
2018-06-25 cs.CC cs.LO
Linear-time Temporal Logic with Team Semantics: Expressivity and Complexity
研究了具有团队语义的模型检验线性时态逻辑（TeamLTL）的表达性和复杂性。TeamLTL，尽管是一个纯粹的模态逻辑，但能够定义超属性，即，与多个执行跟踪相关的属性。TeamLTL最近才被引入，关于它的表达能力和模型检验问题，只有很少的结果是已知的。我们将TeamLTL的表达性与通过用迹和命题量词（HyperLTL和HyperQPTL）扩展LTL获得的超性质的逻辑联系起来。通过这样做，我们得到了一些模型检验的TeamLTL结果，并确定其不可判定性边界。特别是，我们证明了任何向下封闭的TeamLTL扩展的所谓的左平坦片段的模型检验的可判定性。此外，我们建立了具有布尔析取和包含原子的TeamLTL的模型检验问题是不可判定的。
2021-11-23 cs.CC cs.LO
Propositional Dynamic Logic for Hyperproperties
反应式系统的信息安全属性（如非干扰性）通常需要将系统的不同执行相互关联并同时遵循它们。这样的超性质在其他上下文中也可以是有用的，例如，当分析分布式系统的属性时，如线性化。由于LTL、CTL或模态μ演算等常见逻辑无法表达超性质，因此开发了超逻辑HyperLTL和HyperCTL* 来解决这个缺陷。然而，这些逻辑不能表达任意的Ω-正则性质。在本文中，我们介绍HyperPDL-三角洲，一个适应的命题动态逻辑的Fischer和Ladner的hyperproperties，为了消除这一限制。使用一个优雅的自动机理论框架，我们表明，HyperPDL-三角洲模型检验是渐近不更昂贵的HyperCTL* 模型检验，尽管它大大增加了表达能力。我们进一步研究片段的HyperPDL-三角洲方面的可满足性检查。
2020-07-17 cs.FL cs.LO
Software Verification of Hyperproperties Beyond k-Safety
时态超属性是与多个执行跟踪相关的系统属性。对于（有限状态）硬件，时态超属性由模型检验算法支持，并且存在用于一般时态逻辑的工具，如HyperLTL。对于（无限状态）软件，到目前为止，时间超属性的分析仅限于$k$ -安全属性，即，规定任何$k$迹线之间不存在不良交互的属性。在本文中，我们提出了一个自动化的方法来验证$\forall^k\exists^l$ -安全性质的无限状态系统。$\forall^k\exists^l$ -安全属性规定，对于任何$k$迹线，存在$l$迹线，使得所得到的$k+l$迹线不会不良地交互。这种泛量化和存在量化的结合使我们能够表达$k$ -安全性之外的许多性质，包括例如广义不干涉或程序细化。我们的方法是基于一个基于策略的实例化的存在跟踪量化相结合的程序减少，无论是在一个固定的谓词抽象的上下文中。值得注意的是，我们的框架允许战略和减少的相互依赖。
2022-08-25 cs.LO
Logics for Context-free Hyperproperties
Technische Universität Ilmenau（伊尔梅瑙工业大学）；Université Paris Cité, CNRS, IRIF（巴黎西岱大学，法国国家科学研究中心，信息研究与研究所）；Aalborg University（奥尔堡大学）
提出一种用于指定上下文无关超性质的逻辑，通过迹量化扩展可视下推自动机，并证明单量词交替下的模型检测可判定性及不可判定性边界。
2026-10-04 cs.FL cs.LO
Prophecy Variables for Hyperproperty Verification
像HyperLTL这样的超属性的时态逻辑使用跟踪量词来表达与多个系统运行相关的属性。在实践中，这种规范的验证大多限于没有量词交替的公式，其中验证可以减少到检查系统的自组成上的跟踪属性。像$\forall π. \exists π'. ϕ$这样的量词替换可以通过互补来解决，也可以解释为$\forall$ -玩家和$\exists$-玩家之间的双人游戏，$\forall$ -玩家递增地构建轨迹$π$，$\exists$ -玩家以这样的方式构建$π'$，即$π$和$π'$一起满足$ϕ$。基于游戏的方法明显便宜但不完整，因为$\exists$玩家不知道$\forall$玩家的未来移动。在本文中，我们建立了游戏为基础的方法，可以通过添加（$ω$定期）时间预言完成。我们的证明是建设性的，产生一个有效的算法生成一套完整的预言。
2022-06-03 cs.CR cs.LO
