Checking Satisfiability of Hyperproperties using First-Order Logic
CISPA Helmholtz Center for Information Security（CISPA亥姆霍兹信息安全中心）
本文提出FOLHyper工具，通过将超属性问题转化为一阶逻辑公式，实现对超属性可满足性的自动检查，扩展了HyperLTL的分析范围。
2025-12-29 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
A Temporal Logic for Asynchronous Hyperproperties
超性质是计算系统的性质，其需要多于一个迹来评估，例如，许多信息流安全性和并发性要求。在跟踪属性定义一组跟踪的情况下，超属性定义一组多组跟踪。时态逻辑HyperLTL和HyperCTL* 已经被提出来表达超属性。然而，它们的语义是同步的，因为所有跟踪都以相同的速度进行，并在相同的位置进行评估。这就排除了使用这些逻辑来分析其轨迹可以以不同速度进行的系统，并允许不同的轨迹独立地采取断续步骤。为了解决这个问题，在本文中，我们提出了一个异步变体的HyperLTL。在消极的一面，我们表明，这种变体的模型检查问题是不可判定的。在积极的一面，我们确定了一个可判定的片段，其中涵盖了丰富的公式与实际应用。我们还提出了两个模型检测算法，减少我们的问题的同步语义的HyperLTL模型检测问题。
2021-04-28 cs.LO
Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)
本文提出将断言提升至任意状态集合性质的超霍尔逻辑，可在同一框架内证明和否证包括现有逻辑无法表达的任意程序超性质，且已证明其可靠性与完备性，所有结果均在Isabelle/HOL中验证。
2024-04-11 cs.LO
RVHyper: A Runtime Verification Tool for Temporal Hyperproperties
我们提出RVHyper，一个运行时验证工具的hyperproperties。超性质，如非干涉性和观察决定论，将多个计算轨迹相互关联。规范在时态逻辑HyperLTL中以公式的形式给出，它扩展了线性时间时态逻辑（LTL）的跟踪量词和跟踪变量。RVHyper按顺序处理执行跟踪，直到检测到违反规范。在这种情况下，将返回一组跟踪形式的反例。作为一个示例应用程序，我们展示了如何RVHyper可以用来检测虚假的依赖关系，在硬件设计。
2019-05-31 cs.LO
Disintegration Temporal Logic for Probabilistic Hyperproperties
CISPA Helmholtz Center for Information Security（CISPA 亥姆霍兹信息安全中心）；Technical University of Munich（慕尼黑工业大学）
研究提出分解时态逻辑（DTL）用于表达概率超属性，基于测度分解概念支持对随机系统推理。阐述其在多方面应用及与现有逻辑关系，虽完整DTL模型检查不可判定，但确定两个可判定片段，线性片段基于线性代数技术，定性片段扩展标准算法。
2026-07-17 cs.LO
Second-Order Hyperproperties
本文提出支持对迹集合进行二阶量化的时间逻辑Hyper$^2$LTL，以表达公共知识等复杂超性质，并针对受限片段设计了基于不动点迭代和自动机学习的近似模型检测算法，在工具HySO中验证有效。
2023-05-29 cs.LO
Explainability Requirements as Hyperproperties
CISPA Helmholtz Center for Information Security（CISPA 亥姆霍兹信息安全中心）
本文结合 Lewis 反事实条件句、LTL 与知识模态词形式化多智能体系统的反事实可解释性，并将其嵌入超逻辑，证明模型检测可判定。
2025-10-18 cs.LO
Monitoring hyperproperties with circuits
本文根据Hyper-LTL的思想，给出了Hennessy-Milner逻辑安全片段的一种扩展，它具有迹集上的递归性。然后，它介绍了一种新的监测设置，采用类似电路的结构，结合定期监测的判决。这项研究的主要贡献是监测和他们的语义本身，以及一个监测合成程序从公式的逻辑，产生“电路样监测”的这种类型的声音和违反完成了一个有限的一组无限的痕迹。
2022-05-10 cs.LO
Program Repair for Hyperproperties
我们研究了时态逻辑HyperLTL中指定的超属性的修复问题。超属性是与多个计算轨迹相关的系统属性。这类属性包括信息流策略，如不干涉和观察决定论。修复问题是为给定的Kripke结构找到满足给定规范的子结构。我们发现，修复问题是可判定的HyperLTL规格和有限状态Kripke结构。我们提供了一个详细的复杂性分析不同片段的HyperLTL和不同的系统类型：树形，非循环，和一般的Kripke结构。
2021-01-19 cs.LO
Statistical Verification of Hyperproperties for Cyber-Physical System
信息物理系统（CPS）的许多重要属性都是基于连续时间内多个执行之间的关系来定义的。示例包括概率公平性和对建模误差的敏感性（即，参数变化）。这些要求只能由hyperproperties指定。在这项工作中，我们专注于验证CPS的概率超性质。为了涵盖广泛的建模形式主义，我们首先提出了一个通用的概率不确定系统（PUSs）模型，统一了通常研究的CPS模型，如连续时间马尔可夫链（CTMCs）和概率参数化混合I/O自动机。为了正式指定hyperproperties，我们提出了一个新的时序逻辑，超概率信号时序逻辑（HyperPSTL），作为一个超和概率版本的传统信号时序逻辑（STL）。考虑到现实世界中的系统，可以被捕获为PUSs的复杂性，我们采用了统计模型检验（SMC）的方法来验证。我们开发了一种新的SMC技术的基础上直接计算的显着性水平的统计断言的HyperPSTL规范，它不需要先验知识的无差异保证金。然后，我们介绍了SMC算法的HyperPSTL规范的联合概率分布的多条路径，以及规范与嵌套的概率算子量化不同的路径，这不能处理现有的SMC算法。最后，我们证明了我们的SMC算法的有效性CPS基准与不同程度的复杂性，包括丰田动力总成控制系统。
2019-08-06 cs.LO
A Temporal Logic for Hyperproperties
克拉克森和施奈德引入的超属性将计算机程序的正确性描述为其计算路径集的条件。标准时态逻辑一次只能引用一条路径，因此无法表达许多感兴趣的超性质，包括不干涉和安全和编码理论中的其他重要性质。本文研究了具有显式路径变量的时态逻辑的扩展。我们表明，量化的路径自然包含其他扩展的时间逻辑与运营商的信息流和知识。具有路径量化的时序逻辑的模型检验问题是可判定的。对于交替深度1，复杂度在公式长度上是PSPACE，在系统大小上是NLOGSPACE，就像线性时间时态逻辑一样。
2013-06-27 cs.CR 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
The First-Order Logic of Hyperproperties
我们研究了超性质的逻辑基础。超属性将迹属性（迹的集合）推广到迹的集合的集合。超性质最突出的应用是信息流安全：信息流策略通过比较两个或多个执行轨迹来表征系统的秘密性和完整性，例如通过比较外部观察者对由秘密变量的不同值产生的执行轨迹的观察。本文建立了超性质时态逻辑与一阶逻辑之间的第一个联系。坎普的开创性定理（在制定由于Gabbay等人）指出线性时间时态逻辑（LTL）在表达上等价于有序自然数上的一阶逻辑。我们介绍了一阶逻辑的轨迹集，并证明了HyperLTL，LTL的超性质的扩展，是严格包含在这个逻辑。此外，我们展示了一个片段，是表达等价于HyperLTL，从而建立坎普的超性质定理。
2017-01-09 cs.CR cs.LO math.LO
On the Expressive Power of TeamLTL and First-Order Team Logic over Hyperproperties
在这篇文章中，我们研究线性时态逻辑与团队语义（TeamLTL），是新的逻辑定义超属性。我们将这些逻辑的坎普型翻译定义为一阶团队逻辑和二阶逻辑的片段。我们还描述了团队逻辑和二阶逻辑的模型检查和可满足性的表达能力和复杂性，将它们与二阶和三阶算术联系起来。我们的结果集在一个更大的背景下，最近的结果Lück表明，扩展TeamLTL的布尔否定是高度不可判定的下，所谓的同步语义。我们还研究了TeamLTL扩展的口吃不变片段。
2021-10-21 cs.LO math.LO
Deciding Hyperproperties
超性质，如观测决定论或对称性，不能表示为单个计算轨迹的性质，因为它们描述了多个计算轨迹之间的关系。HyperLTL是一种时态逻辑，它通过跟踪变量来捕获这种关系，跟踪变量是通过存在和泛跟踪量词引入的，可以用于同时引用多个计算。本文研究了HyperLTL的可满足性问题。我们发现，这个问题是PSPACE-完全的替代自由的公式（因此，没有比LTL可满足性更昂贵），EXPSPACE-完全的存在，为所有的公式，和undecidable为所有存在的公式。许多实际的超性质可以表示为无择一公式。我们的结果表明，这类性质的可满足性和蕴涵都是可判定的。
2016-06-22 cs.LO
TAPAAL HyperLTL: A Tool for Checking Hyperproperties of Petri Nets
TU Berlin（柏林工业大学）；Aalborg University（奥尔堡大学）
本文提出了一种针对Petri网的HyperLTL模型检查器，用于验证超属性，该工具集成于TAPAAL框架并展示了其在计算机网络领域的应用性能。
2026-01-09 cs.LO
Efficient Monitoring of Hyperproperties using Prefix Trees
超属性，如非干扰和观察决定论，将多个计算轨迹相互关联，因此无法通过孤立考虑计算的工具进行监控。我们提出了在最新版本的RVHyper，运行时验证工具hyperproperties的监测方法。该工具的输入是时序逻辑HyperLTL中给出的规范，HyperLTL扩展了具有跟踪量词和跟踪变量的线性时序逻辑（LTL）。RVHyper按顺序处理执行跟踪，直到检测到违反规范。在这种情况下，将返回一组跟踪形式的反例。RVHyper采用了一系列优化：规范的预处理分析和最大限度地减少监控过程中需要存储的跟踪的过程。在这篇文章中，我们介绍了一种新的跟踪存储技术，安排在一个树状结构的痕迹，利用部分相等的痕迹。我们评估RVhyper现有的基准安全信息流控制，纠错码和对称性的硬件设计。作为安全性之外的一个示例应用程序，我们展示了如何使用RVHyper来检测硬件设计中的虚假依赖关系。
2021-01-18 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
The Hierarchy of Hyperlogics
超性质通过将多个迹联系起来来推广迹的性质，在信息流安全中得到了广泛的研究。最近，已经提出了一些超性质的逻辑，并且需要理解它们的可判定性和相对表达性。新的逻辑已经从标准逻辑中获得了两个主要的扩展：时态逻辑，如LTL和CTL $^*$，已经通过为迹或路径添加变量而被推广到超属性。一阶逻辑和二阶逻辑，如一元一阶序逻辑和MSO，已经用等阶谓词扩展。我们研究了两个扩展的线性时间和分支时间逻辑的频谱的影响，特别是对命题的量化逻辑。由此产生的超逻辑层次结构与经典层次结构有很大不同，这表明等级别谓词比跟踪和路径变量增加了更多的表达能力。在超逻辑的层次结构中，我们确定了可满足性问题的可判定性的新边界。具体来说，我们表明，虽然HyperQPTL和HyperCTL $^*$都是不可判定的一般，公式内的$\exists^*\forall^*$片段是可判定的。
2020-05-12 cs.LO
Unifying Asynchronous Logics for Hyperproperties
本文提出 GHyperLTL_SC 超逻辑框架以统一 HyperLTL 的异步扩展与知识逻辑 KLTL，并给出模型检测可判定且表达力更强的 simple 片段。
2024-10-02 cs.LO
Automata-Based Software Model Checking of Hyperproperties
我们开发了时态流逻辑（TSL）和超时态流逻辑（HyperTSL）模理论的模型检验算法。TSL扩展了线性时序逻辑（LTL）的存储单元，功能和谓词，使其成为一个方便的和表达的逻辑推理软件和其他系统的无限数据域。HyperTSL进一步将TSL扩展到hyperproperties的规范-与多个系统执行相关的属性。因此，HyperTSL可以在软件系统中表达信息流策略，如不干涉。我们用理论扩充了HyperTSL，得到了HyperTSL（T），并建立在LTL软件验证的方法上，得到了TSL和HyperTSL（T）的模型检验算法。这导致了一个合理但不一定完整的算法，用于HyperTSL（T）的forall*exists* 片段中包含的规范。我们的方法构成了第一个软件模型检验算法的时间hyperproperties与量词交替，不依赖于有限状态的抽象。
2023-03-26 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
Strategy Logic, Imperfect Information, and Hyperproperties
CISPA Helmholtz Center for Information Security（CISPA信息安全研究中心）
本文研究不完全信息策略逻辑（SL$_\text{ii}$）与超策略逻辑（HyperSL）的关系，证明在状态公式不嵌套于路径公式的限定下二者等价，给出双向编码方法，揭示不完全信息与超性质的内在关联。
2025-10-04 cs.AI cs.LO cs.MA
The Complexity of Asynchronous HyperLTL
Aalborg University（奥尔堡大学）
本文研究了异步超属性逻辑AHLTL的模型检测和可满足性问题，证明了模型检测等价于二阶算术真值，而可满足性在轨迹存在量化时为Σ₁¹-完全，在轨迹全称量化时为Σ₁¹-困难且属于Σ₂¹。
2026-10-11 cs.LO
Deciding Asynchronous Hyperproperties for Recursive Programs
本文提出一种带新机制识别迹位置的异步超性质逻辑，在保持有限状态模型检测复杂度不变且更具表达力的同时，首次为递归程序超性质模型检测提供了合适方法。
2023-10-25 cs.FL cs.LO cs.PL
Temporal Hyperproperties for Population Protocols
本文研究无限状态系统群体协议的时序超性质，证明一般群体协议的HyperLTL验证不可判定，并指出即时观察子类在不包含next算子时验证可判定（2-EXPSPACE），任何扩展均导致不可判定。
2024-10-15 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
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
MGHyper: Checking Satisfiability of HyperLTL Formulas Beyond the $\exists^*\forall^*$ Fragment
超属性是指多个计算轨迹的属性。这包括许多信息流安全策略，如观察确定性，（广义）不干扰和非推理，以及其他系统属性，如对称性或汉明距离。我们介绍MGHyper，一个自动可满足性检查和模型生成的HyperLTL表示的超属性的工具。与以往的可满足性检查器不同，MGHyper不局限于HyperLTL的可判定$\exists^* \forall^*$片段，而是为全逻辑提供了一个半判定过程。MGHyper的一个重要应用是自动检查不同超性质（以及同一超性质的不同形式化）之间的等价性，并构建反例来反驳某个声称的含义。我们描述了在MGHyper中实现的半决策过程，并报告了从文献中获得的典型超性质和随机生成的HyperLTL公式的实验结果。
2019-03-26 cs.LO
Asynchronous Extensions of HyperLTL
超属性是一种现代规范范式，它扩展了跟踪属性以表达跟踪集的属性。在文献中研究的超属性的时态逻辑，包括HyperLTL，假设一个同步的语义和享受可判定的模型检验问题。在本文中，我们介绍了两个异步和正交扩展的HyperLTL，即口吃HyperLTL（HyperLTLS）和上下文HyperLTL（HyperLTLC）。这两个扩展都很有用，例如，制定信息流安全属性的异步变体。我们表明，对于这些逻辑，模型检验一般是不可判定的。在积极的一面，对于他们中的每一个，我们确定了一个片段与可判定的模型检验，包括HyperLTL，可以表达有意义的异步需求。此外，我们提供了确切的计算复杂性的模型检验这两个片段，HyperLTLS片段，符合严格的表达逻辑HyperLTL。
2021-04-26 cs.LO
Coinductive Proofs for Temporal Hyperliveness
针对时序超性质演绎证明系统匮乏的问题，提出用共归纳关系近似∀*∃*ψ型超性质，构建Coq中的机械化框架HyCo并验证其可靠性与实用性。
2025-01-14 cs.LO cs.PL
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
Model Checking Time Window Temporal Logic for Hyperproperties
University of Missouri-Columbia（密苏里大学哥伦比亚分校）；University of Dayton（代顿大学）
本文提出 HyperTWTL 形式化体系及其同步/异步语义，用于表达多执行迹超性质，并给出通过归约到 TWTL 的模型检测算法，以验证机器人应用中的信息流安全与并发性质。
2023-08-10 cs.FL cs.LO cs.RO
Verifying Asynchronous Hyperproperties in Reactive Systems
CISPA Helmholtz Center for Information Security（CISPA亥姆霍兹信息安全中心）
本文提出了一种基于游戏的方法，用于验证反应系统中任意∀*∃* A-HLTL公式，解决了异步超属性的模型检查问题。
2025-12-29 cs.FL cs.LO cs.PL
Realizing Omega-regular Hyperproperties
研究了超逻辑HyperQPTL，它结合了迹关系和$ω$ -正则性的概念.我们证明了HyperQPTL是非常有表现力的，它可以表达诸如不确定性，有界等待授权，认知属性，特别是任何$ω$ -正则属性等属性。这些属性在以前研究过的超逻辑（如HyperLTL）中无法表达。与此同时，我们认为，HyperQPTL的表现力是最佳的，在某种意义上，一个更有表现力的逻辑$ω$ -正则超属性将有一个不可判定的模型检验问题。我们进一步研究了HyperQPTL的可实现性问题。我们证明了可实现性对于包含像不确定性这样的属性的HyperQPTL片段是可判定的。但是，与可满足性问题相比，命题量化确实使超逻辑的可实现性问题更难。更具体地说，具有泛存在命题量词交替后跟单个迹量词的HyperQPTL公式片段通常是不可判定的，即使片段到HyperLTL的投影具有可判定的可实现性问题。最后，我们在原型工具BoSy中实现了HyperQPTL的有界综合问题。使用带有HyperQPTL规范的BoSy，我们已经能够合成几个资源仲裁器。非线性时间超逻辑的综合问题仍然是一个未解决的问题。例如，还不知道如何从分支时间超逻辑（如HyperCTL $^*$）中给出的规范合成系统。
2021-01-18 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
Automata and Fixpoints for Asynchronous Hyperproperties
在过去的十年中，由于它们的重要性，超性质受到越来越多的关注，例如安全分析。过去的方法都集中在同步分析，即技术，其中不同的路径进行比较锁定逐步。本文通过引入一种新的自动机模型（Alternating Asynchronous Parity Automata）和时间不动点演算$\Hmu$，系统地研究了超性质的异步分析.我们表明，这两种模式的表达能力相一致的固定路径分配。这两个模型的高表达能力证明了这样一个事实，即决策问题的利益是高度不可判定的，即，甚至不是算术。作为一种补救措施，我们提出了近似分析这两种模式，也引起自然可判定的片段。
2020-10-22 cs.FL cs.LO cs.PL
Temporal Team Semantics Revisited
本文提出基于时间评估函数的时间团队语义学，用于规范异步超属性，并证明同步TeamLTL的嵌入、某些TeamCTL片段MC的高度不可判定性，以及TeamCTL*到交替异步Büchi自动机的翻译及可判定性结果。
2024-02-05 cs.CC cs.LO
Deciding branching hyperproperties for real time systems
本文研究实时系统分支超性质的判定问题，提出度量时序逻辑的分支超性质扩展HCMTL*，证明其在时间自动机上的验证不可判定，限定固定时间范围时可通过归约为有界实数域MSO问题实现可判定。
2024-05-20 cs.CR cs.LO
A Remark on the Expressivity of Asynchronous TeamLTL and HyperLTL
本文研究异步TeamLTL与HyperLTL的表达力关系，证明TeamLTL的布尔析取扩展等价于单全称量词HyperLTL的正布尔闭包，其布尔否定扩展的左向下封闭片段等价于对应布尔闭包。
2024-06-07 cs.LO
On Hyperproperty Verification, Quantifier Alternations, and Games under Partial Information
针对含任意量词交替的超属性验证难题，提出利用部分信息下的层级多人博弈方法，证明其可判定性，拓展了博弈法的适用范围。
2025-10-04 cs.LO
Gray-box Monitoring of Hyperproperties (Extended Version)
许多重要的系统属性，特别是安全性和隐私性，无法静态验证。因此，运行时验证是一个有吸引力的替代方案。超属性的逻辑，如HyperLTL，支持一组丰富的此类属性。我们首先表明，黑盒监控HyperLTL一般是不可行的，并建议灰盒的方法。灰盒监控意味着在运行时对系统进行分析，这给可监控性（解决监控问题的可行性）带来了新的限制。因此，作为本文的另一个贡献，我们完善了经典的概念monitorability，无论是跟踪性能和hyperproperties，考虑到可计算的监视器。然后，我们应用我们的方法来监控一个隐私hyperproperty称为分布式数据最小化，表示为一个HyperLTL属性，通过使用基于SMT的静态验证器在运行时。
2019-10-04 cs.CR cs.FL cs.LO
HyperCertificates: Verification of Discrete-time Dynamical Systems against HyperLTL Specifications
University of Colorado Boulder（科罗拉多大学博尔德分校）
本文提出一种归纳框架，通过超证书概念验证离散时间动态系统 against 超LTL规范。方法结合前瞻函数与屏障函数，利用闭包证书和SOS/SMT技术实现自动验证。
2026-05-01 cs.LO cs.SY eess.SY
Strategic Dominance: A New Preorder for Nondeterministic Processes
该研究提出非确定性状态转换模型间的新预序strategic dominance，证明其介于迹包含与树包含之间，可用resolver logic在2-ExpTime内检验，并拓展了该逻辑的多类应用场景。
2024-07-15 cs.LO
Verifying Security Policies in Multi-agent Workflows with Loops
我们认为基于Web的工作流，如会议提交系统，如EasyChair的信息流安全策略的自动验证。我们的工作流描述语言允许循环，非确定性的选择，和无限数量的参与代理。信息流策略在超属性的时态逻辑中指定。我们证明了验证问题可以归结为一阶线性时间时序逻辑公式的可满足性，并为相关类别的工作流和规范提供可判定性结果。我们报告的一系列基准上实现我们的方法所获得的实验结果。
2017-08-29 cs.CR cs.LO
The Program Logic of Abstract Interpretation
Department of Mathematics, University of Padua（帕多瓦大学数学系）；Department of Computer Science, University of Pisa（比萨大学计算机系）
本文提出APPL逻辑，统一了Hoare逻辑、错误逻辑和超Hoare逻辑变体，提供抽象程序逻辑的理论基础，支持多种抽象域。
2026-11-09 cs.LO cs.PL
Hyperproperty-Constrained Secure Reinforcement Learning
Bayloy University（贝勒大学）；University of Dayton（代顿大学）；University of Missouri-Columbia（密苏里大学哥伦比亚分校）
针对现有强化学习研究缺乏超属性层面安全约束的问题，提出在满足HyperTWTL安全规约的同时用动态Boltzmann softmax RL学习最优策略的方法，经机器人任务验证优于基线算法。
2025-07-31 cs.AI cs.LG cs.LO
Verifying Hyperliveness
HyperLTL是线性时间时态逻辑的扩展，用于规范超属性，即，与多个计算轨迹相关的时间属性。HyperLTL可以表达信息流策略以及互斥算法中的对称性或抗错误传输协议中的汉明距离等属性。以前的工作对HyperLTL模型检验的重点是替代自由片段的HyperLTL，其中验证减少到检查一个标准的跟踪属性在一个适当的自我组成的系统。然而，无替代片段并不涵盖一般的超活性属性。例如，通用公式不能表达保密要求，即对于秘密变量的每一个可能值，都存在一个计算，其中值是不同的，而外部观察者所做的观察是相同的。在本文中，我们研究了更困难的情况下，hyperliveness属性表示为HyperLTL公式与量词交替。我们减少存在量化的战略选择，并表明合成算法可以用来消除存在量词自动。我们还表明，这种方法可以扩展到反应系统的合成，即，自动构建一个反应系统，保证满足给定的HyperLTL公式。
2020-05-15 cs.LO
HyPOLE: Hyperproperty-Guided Multi-Agent Reinforcement Learning under Partial Observation
提出HyPOLE框架，利用超属性逻辑HyperLTL在部分观测下引导多智能体强化学习，结合CTDE合成去中心化策略，在多个基准上优于基线方法。
2026-07-01 cs.AI cs.LO cs.MA
Bayesian Statistical Model Checking for Multi-agent Systems using HyperPCTL*
Kansas State University（堪萨斯州立大学）
在本文中，我们提出了一个贝叶斯方法的统计模型检验（SMC）的概率超性质的逻辑HyperPCTL* 上的离散时间马尔可夫链（DTMCs）。虽然SMC的HyperPCTL* 使用序贯概率比检验（SPRT）已经探索过，我们开发了一种替代SMC算法的基础上贝叶斯假设检验。与PCTL* 相比，验证HyperPCTL* 公式是复杂的，因为它们在DTMC的多个路径上同时解释。此外，由于SMC不返回子公式的可满足性问题的精确答案，而是仅返回具有高置信度的正确答案，因此扩展非概率设置的自底向上模型检查算法并不直接。我们提出了一个递归算法的SMC的HyperPCTL* 的基础上修改贝叶斯检验，在递归可满足性结果的不确定性的因素。我们已经实现了我们的算法在Python工具箱，HyProVer，并比较我们的方法与基于SPRT的SMC。我们的实验评估表明，我们的贝叶斯SMC算法在验证时间和推导给定HyperPCTL* 公式的可满足性所需的样本数量方面都表现得更好。
2022-09-06 cs.AI cs.LO cs.MA
