A Temporal Logic for Asynchronous Hyperproperties
超性质是计算系统的性质，其需要多于一个迹来评估，例如，许多信息流安全性和并发性要求。在跟踪属性定义一组跟踪的情况下，超属性定义一组多组跟踪。时态逻辑HyperLTL和HyperCTL* 已经被提出来表达超属性。然而，它们的语义是同步的，因为所有跟踪都以相同的速度进行，并在相同的位置进行评估。这就排除了使用这些逻辑来分析其轨迹可以以不同速度进行的系统，并允许不同的轨迹独立地采取断续步骤。为了解决这个问题，在本文中，我们提出了一个异步变体的HyperLTL。在消极的一面，我们表明，这种变体的模型检查问题是不可判定的。在积极的一面，我们确定了一个可判定的片段，其中涵盖了丰富的公式与实际应用。我们还提出了两个模型检测算法，减少我们的问题的同步语义的HyperLTL模型检测问题。
2021-04-28 cs.LO
HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
本文提出HyperATL*逻辑，通过引入路径变量和策略量词扩展计算树逻辑，支持在多智能体系统中对战略能力进行推理，统一捕获多种安全概念，并证明了其有穷状态模型检测的可判定性与算法渐近最优性。
2023-05-30 cs.LO
RVHyper: A Runtime Verification Tool for Temporal Hyperproperties
我们提出RVHyper，一个运行时验证工具的hyperproperties。超性质，如非干涉性和观察决定论，将多个计算轨迹相互关联。规范在时态逻辑HyperLTL中以公式的形式给出，它扩展了线性时间时态逻辑（LTL）的跟踪量词和跟踪变量。RVHyper按顺序处理执行跟踪，直到检测到违反规范。在这种情况下，将返回一组跟踪形式的反例。作为一个示例应用程序，我们展示了如何RVHyper可以用来检测虚假的依赖关系，在硬件设计。
2019-05-31 cs.LO
Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version)
本文提出将断言提升至任意状态集合性质的超霍尔逻辑，可在同一框架内证明和否证包括现有逻辑无法表达的任意程序超性质，且已证明其可靠性与完备性，所有结果均在Isabelle/HOL中验证。
2024-04-11 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
The First-Order Logic of Hyperproperties
我们研究了超性质的逻辑基础。超属性将迹属性（迹的集合）推广到迹的集合的集合。超性质最突出的应用是信息流安全：信息流策略通过比较两个或多个执行轨迹来表征系统的秘密性和完整性，例如通过比较外部观察者对由秘密变量的不同值产生的执行轨迹的观察。本文建立了超性质时态逻辑与一阶逻辑之间的第一个联系。坎普的开创性定理（在制定由于Gabbay等人）指出线性时间时态逻辑（LTL）在表达上等价于有序自然数上的一阶逻辑。我们介绍了一阶逻辑的轨迹集，并证明了HyperLTL，LTL的超性质的扩展，是严格包含在这个逻辑。此外，我们展示了一个片段，是表达等价于HyperLTL，从而建立坎普的超性质定理。
2017-01-09 cs.CR cs.LO math.LO
A Temporal Logic for Hyperproperties
克拉克森和施奈德引入的超属性将计算机程序的正确性描述为其计算路径集的条件。标准时态逻辑一次只能引用一条路径，因此无法表达许多感兴趣的超性质，包括不干涉和安全和编码理论中的其他重要性质。本文研究了具有显式路径变量的时态逻辑的扩展。我们表明，量化的路径自然包含其他扩展的时间逻辑与运营商的信息流和知识。具有路径量化的时序逻辑的模型检验问题是可判定的。对于交替深度1，复杂度在公式长度上是PSPACE，在系统大小上是NLOGSPACE，就像线性时间时态逻辑一样。
2013-06-27 cs.CR cs.LO
Second-Order Hyperproperties
本文提出支持对迹集合进行二阶量化的时间逻辑Hyper$^2$LTL，以表达公共知识等复杂超性质，并针对受限片段设计了基于不动点迭代和自动机学习的近似模型检测算法，在工具HySO中验证有效。
2023-05-29 cs.LO
Explainability Requirements as Hyperproperties
本文结合 Lewis 反事实条件句、LTL 与知识模态词形式化多智能体系统的反事实可解释性，并将其嵌入超逻辑，证明模型检测可判定。
2025-10-18 cs.LO
Synthesizing Reactive Systems from Hyperproperties
我们研究的反应合成问题的超性质的时态逻辑HyperLTL的公式。超性质概括了迹性质，即，成组的轨迹，成组的轨迹典型的例子是信息流政策，如不干涉政策，规定任何敏感数据都不能泄露到公共领域。这些属性不能用标准的线性或分支时间时态逻辑（如LTL、CTL或CTL $^*$）来表示。我们发现，虽然合成问题是不可判定的完整的HyperLTL，它仍然是可判定的$\exists^*$，$\exists^*\forall^1$，和$\mathit{linear}\;\forall^*$片段。在这些片段之外，合成问题立即变得不可判定。对于通用HyperLTL，我们提出了一个半决策过程，构造实现和反例到一个给定的界限。我们报告了令人鼓舞的实验结果，如对称响应，保密性和信息流的超特性的示例规范的原型实现。
2019-05-31 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
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
Monitoring hyperproperties with circuits
本文根据Hyper-LTL的思想，给出了Hennessy-Milner逻辑安全片段的一种扩展，它具有迹集上的递归性。然后，它介绍了一种新的监测设置，采用类似电路的结构，结合定期监测的判决。这项研究的主要贡献是监测和他们的语义本身，以及一个监测合成程序从公式的逻辑，产生“电路样监测”的这种类型的声音和违反完成了一个有限的一组无限的痕迹。
2022-05-10 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
Controller Synthesis for Hyperproperties
我们研究的问题，控制器合成的时间逻辑HyperLTL中指定的超属性。超属性是与多个执行跟踪相关的系统属性。超属性可以优雅地表达信息流策略，如不干涉和观察决定论。控制器综合问题是自动设计一个控制器的工厂，确保满足给定的规格在存在的环境或敌对行动。我们表明，控制器综合问题是可判定的HyperLTL规格和有限状态的植物。我们提供了一个严格的复杂性分析不同片段的HyperLTL和不同的系统类型：树形，无环，和一般的图形。
2021-01-19 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
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
Temporal Hyperproperties for Population Protocols
本文研究无限状态系统群体协议的时序超性质，证明一般群体协议的HyperLTL验证不可判定，并指出即时观察子类在不包含next算子时验证可判定（2-EXPSPACE），任何扩展均导致不可判定。
2024-10-15 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
TAPAAL HyperLTL: A Tool for Checking Hyperproperties of Petri Nets
TU Berlin（柏林工业大学）；Aalborg University（奥尔堡大学）
本文提出了一种针对Petri网的HyperLTL模型检查器，用于验证超属性，该工具集成于TAPAAL框架并展示了其在计算机网络领域的应用性能。
2026-01-09 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
Efficient Monitoring of Hyperproperties using Prefix Trees
超属性，如非干扰和观察决定论，将多个计算轨迹相互关联，因此无法通过孤立考虑计算的工具进行监控。我们提出了在最新版本的RVHyper，运行时验证工具hyperproperties的监测方法。该工具的输入是时序逻辑HyperLTL中给出的规范，HyperLTL扩展了具有跟踪量词和跟踪变量的线性时序逻辑（LTL）。RVHyper按顺序处理执行跟踪，直到检测到违反规范。在这种情况下，将返回一组跟踪形式的反例。RVHyper采用了一系列优化：规范的预处理分析和最大限度地减少监控过程中需要存储的跟踪的过程。在这篇文章中，我们介绍了一种新的跟踪存储技术，安排在一个树状结构的痕迹，利用部分相等的痕迹。我们评估RVhyper现有的基准安全信息流控制，纠错码和对称性的硬件设计。作为安全性之外的一个示例应用程序，我们展示了如何使用RVHyper来检测硬件设计中的虚假依赖关系。
2021-01-18 cs.LO
Deciding Asynchronous Hyperproperties for Recursive Programs
本文提出一种带新机制识别迹位置的异步超性质逻辑，在保持有限状态模型检测复杂度不变且更具表达力的同时，首次为递归程序超性质模型检测提供了合适方法。
2023-10-25 cs.FL cs.LO cs.PL
The Hierarchy of Hyperlogics
超性质通过将多个迹联系起来来推广迹的性质，在信息流安全中得到了广泛的研究。最近，已经提出了一些超性质的逻辑，并且需要理解它们的可判定性和相对表达性。新的逻辑已经从标准逻辑中获得了两个主要的扩展：时态逻辑，如LTL和CTL $^*$，已经通过为迹或路径添加变量而被推广到超属性。一阶逻辑和二阶逻辑，如一元一阶序逻辑和MSO，已经用等阶谓词扩展。我们研究了两个扩展的线性时间和分支时间逻辑的频谱的影响，特别是对命题的量化逻辑。由此产生的超逻辑层次结构与经典层次结构有很大不同，这表明等级别谓词比跟踪和路径变量增加了更多的表达能力。在超逻辑的层次结构中，我们确定了可满足性问题的可判定性的新边界。具体来说，我们表明，虽然HyperQPTL和HyperCTL $^*$都是不可判定的一般，公式内的$\exists^*\forall^*$片段是可判定的。
2020-05-12 cs.LO
Model Checking Quantitative Hyperproperties
超性质是计算迹集的性质。在本文中，我们研究了定量超性质，我们定义为超性质，表示在一定的关系可能出现的迹的数量上的界限。例如，定量非干扰限制了通过系统的可观察输出泄露的关于某些秘密输入的信息量。因此，定量非干扰限制了具有相同可观察输入但不同可观察输出的迹线的数量。我们研究的设置HyperLTL，超性质的时间逻辑的定量超性质。我们表明，虽然定量超性能可以表示在HyperLTL，运行时间的HyperLTL模型检验算法是，根据属性的类型，指数，甚至双指数的定量界。我们改进了这种复杂性与一个新的模型检验算法的基础上模型计数。新算法只需要对数空间的界限，因此，根据属性，指数甚至双指数超过模型检验算法的HyperLTL。在最坏的情况下，新算法需要多项式空间的系统的大小。我们的最大#SAT为基础的原型实现表明，然而，计数方法是可行的系统与非平凡的定量信息流的要求，如密码检查。
2019-05-31 cs.LO
Unifying Asynchronous Logics for Hyperproperties
本文提出 GHyperLTL_SC 超逻辑框架以统一 HyperLTL 的异步扩展与知识逻辑 KLTL，并给出模型检测可判定且表达力更强的 simple 片段。
2024-10-02 cs.LO
Coinductive Proofs for Temporal Hyperliveness
针对时序超性质演绎证明系统匮乏的问题，提出用共归纳关系近似∀*∃*ψ型超性质，构建Coq中的机械化框架HyCo并验证其可靠性与实用性。
2025-01-14 cs.LO cs.PL
Monitoring Hyperproperties
超属性，如非干扰性和观察确定性，将多个系统执行相互关联。它们不能用标准的时态逻辑（如LTL、CTL和CTL*）来表示，因此不能用标准的运行时验证技术来监视。HyperLTL扩展了线性时间时态逻辑（LTL），在迹上显式量化，以表达Hyperproperties。我们研究了HyperLTL公式在三种不同输入模型下的运行时验证问题：（1）并行模型，其中并行处理固定数量的系统执行。(2)无限顺序模型，其中系统执行是顺序处理的，每次一个执行。在这个模型中，传入执行的数量可能会永远增长。(3)有界顺序模型，其中跟踪按顺序处理，传入执行的数量是有界的。我们证明了对于输入模型（1）和（3），决定HyperLTL公式的可监控性是PSPACE完全的。对于输入模型（2）中的无替代HyperLTL公式，判定可监控性是PSPACE完全的。对于每个输入模型，我们都提供了实用的监控算法。我们还提出了各种优化技术。通过识别规范的属性，如自反性，对称性和传递性，我们减少了跟踪之间的比较次数。对于顺序模型，我们提出了一种技术，最大限度地减少了需要存储的痕迹的数量。最后，我们提供了一个优化，简洁地表示存储的痕迹共享共同的前缀。我们评估了我们的优化，表明这会导致更可扩展的监控，特别是显着降低内存消耗。
2018-07-02 cs.LO
On the Complexity of Linear Temporal Logic with Team Semantics
在线性时序逻辑（LTL）中，一个以公式形式给出的规范通过一组迹来定义一个系统。然而，某些功能，如信息流的安全约束，而不是作为所谓的hyperproperties，这是一套套的痕迹。一种逻辑方法是团队逻辑，这是一个逻辑框架，用于规范信息的依赖性和独立性。团队语义的LTL最近被发现是超属性的逻辑。我们研究了具有同步团队语义和布尔否定的LTL的复杂性理论，证明了LTL的模型检验和可满足性问题都是高度不可判定的，等价于三阶算术的判定问题.此外，我们证明，这种复杂性已经出现在小的时间深度和只有“未来”模态F。最后，我们还介绍了口吃不变性的团队语义推广。
2020-04-27 cs.LO
The Complexity of Asynchronous HyperLTL
Aalborg University（奥尔堡大学）
本文研究了异步超属性逻辑AHLTL的模型检测和可满足性问题，证明了模型检测等价于二阶算术真值，而可满足性在轨迹存在量化时为Σ₁¹-完全，在轨迹全称量化时为Σ₁¹-困难且属于Σ₂¹。
2026-10-11 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
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
Verifying Asynchronous Hyperproperties in Reactive Systems
CISPA Helmholtz Center for Information Security（CISPA亥姆霍兹信息安全中心）
本文提出了一种基于游戏的方法，用于验证反应系统中任意∀*∃* A-HLTL公式，解决了异步超属性的模型检查问题。
2025-12-29 cs.FL cs.LO cs.PL
The Complexity of Monitoring Hyperproperties
我们研究了超属性的运行时验证，表示在时态逻辑HyperLTL，作为一种手段来检查系统的安全策略。超属性的跟踪监视器分析以树形Kripke结构的形式由公共前缀组织的跟踪日志，或者以非循环Kripke结构的形式由公共前缀和公共后缀组织的跟踪日志。与跟踪属性的运行时验证技术不同，监视器跟踪规范的状态，但通常不需要存储跟踪，超属性的监视器重复模型检查不断增长的Kripke结构。这就要求对树型和非循环Kripke结构的模型检验问题进行严格的复杂性分析。我们表明，对于树，Kripke结构的大小的复杂性是L-完全的，独立于HyperLTL公式中的量词交替的数量。对于非循环Kripke结构，复杂度是PSPACE完全的（在对应于量词交替数量的多项式层次结构的级别中）。Kripke结构的大小和HyperLTL公式的长度的组合复杂度对于树和非循环Kripke结构都是PSPACE完全的，并且对于树和无交替HyperLTL公式的相关情况低至NC。因此，Kripke结构和公式的大小和形状对模型检验问题的复杂性具有显著影响。
2021-01-19 cs.LO
Asynchronous Extensions of HyperLTL
超属性是一种现代规范范式，它扩展了跟踪属性以表达跟踪集的属性。在文献中研究的超属性的时态逻辑，包括HyperLTL，假设一个同步的语义和享受可判定的模型检验问题。在本文中，我们介绍了两个异步和正交扩展的HyperLTL，即口吃HyperLTL（HyperLTLS）和上下文HyperLTL（HyperLTLC）。这两个扩展都很有用，例如，制定信息流安全属性的异步变体。我们表明，对于这些逻辑，模型检验一般是不可判定的。在积极的一面，对于他们中的每一个，我们确定了一个片段与可判定的模型检验，包括HyperLTL，可以表达有意义的异步需求。此外，我们提供了确切的计算复杂性的模型检验这两个片段，HyperLTLS片段，符合严格的表达逻辑HyperLTL。
2021-04-26 cs.LO
Efficient Loop Conditions for Bounded Model Checking Hyperproperties
有界模型检验（BMC）是一种通过增量式地探索系统状态空间来发现缺陷的有效技术。为了通过有限的结构推理无限的轨迹并最终获得完整性，BMC结合了重新访问先前观察到的状态的循环条件。本文着重于开发循环条件BMC的HyperLTL-时间逻辑的hyperproperties，允许表达重要的政策，在并发系统的安全性和一致性，等等。循环条件HyperLTL比LTL更复杂，因为不同的轨迹可能会不一致地在不相关的时刻循环。HyperLTL的现有BMC方法仅考虑线性展开，而没有任何循环能力，这排除了找到小的无限迹线和获得完整的技术。我们调查循环条件HyperLTL BMC，其中HyperLTL公式可以包含多达一个量词交替。我们首先提出了一个一般的完全自动机为基础的技术，这是基于最大展开的界限。然后，我们引入替代的基于模拟的算法，允许有效地利用短循环，生成SAT查询，其满足性保证了原始模型检验问题的结果。我们还报告了使用Z3 py的BMC技术的原型实现的经验评估。
2023-01-26 cs.LO
Statistical Verification of Quantitative Hyperproperties: Beyond Boolean Quantification
Chalmers University of Technology（查尔姆斯理工大学）；University of Gothenburg（哥德堡大学）
本文针对现有超性质形式体系无法处理系统定量特性的问题，提出定量超逻辑（QHL），开发其统计验证算法，结合统计方法为嵌套测度量词提供验证方案，在定量IFC基准上验证了方法的表达性与有效性。
2026-08-05 cs.LO
Visualizing Game-Based Certificates for Hyperproperty Verification
针对超属性验证缺乏可信证书的问题，提出将HyperLTL子集超属性的验证转化为量词博弈、以存在量词策略为证书的方法，并开发可视化工具HyGaViz支持交互式探索见证策略。
2025-01-17 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
Automata and Fixpoints for Asynchronous Hyperproperties
在过去的十年中，由于它们的重要性，超性质受到越来越多的关注，例如安全分析。过去的方法都集中在同步分析，即技术，其中不同的路径进行比较锁定逐步。本文通过引入一种新的自动机模型（Alternating Asynchronous Parity Automata）和时间不动点演算$\Hmu$，系统地研究了超性质的异步分析.我们表明，这两种模式的表达能力相一致的固定路径分配。这两个模型的高表达能力证明了这样一个事实，即决策问题的利益是高度不可判定的，即，甚至不是算术。作为一种补救措施，我们提出了近似分析这两种模式，也引起自然可判定的片段。
2020-10-22 cs.FL cs.LO cs.PL
Explaining Hyperproperty Violations
超属性将多个计算轨迹相互关联。因此，在系统模型违反规范的情况下，超属性的模型检查器返回一组作为反例的跟踪。修复系统中导致反例的轨迹之间的错误关系是一项困难的手动工作，可以从额外的解释中获益匪浅。在本文中，我们提出了一种解释方法的反例描述的规格说明逻辑HyperLTL的超性质。我们扩展Halpern和珍珠的定义的实际因果关系的一套痕迹见证了违反HyperLTL公式，这使我们能够识别的事件，造成了违反。我们报告我们的方法的实施，并表明它显着改善了以前的方法，用于分析HyperLTL模型检查器返回的反例。
2022-06-04 cs.LO
Syntax-Guided Automated Program Repair for Hyperproperties
针对无限状态程序的 HyperLTL 时序超性质，提出结合符号执行、约束生成与 SyGuS 的迭代透明修复方法，以生成贴近原程序行为的补丁，原型实验结果良好。
2024-08-12 cs.LO cs.PL
On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing
CISPA Helmholtz Center for Information Security（CISPA亥姆霍兹信息安全中心）
针对交替时间时序逻辑ATL$^*$无法比较多策略交互、无法要求智能体共策略的局限，提出扩展逻辑HyperATL$^*_S$，支持超性质下的策略交互比较与策略共享，证明其模型检测可判定并实现工具HyMASMC完成基准评估。
2024-03-12 cs.AI cs.LO cs.MA
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
Temporal Team Semantics Revisited
本文提出基于时间评估函数的时间团队语义学，用于规范异步超属性，并证明同步TeamLTL的嵌入、某些TeamCTL片段MC的高度不可判定性，以及TeamCTL*到交替异步Büchi自动机的翻译及可判定性结果。
2024-02-05 cs.CC 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
A Temporal Logic of Security
提出了一种新的安全策略验证逻辑。该逻辑HyperLTL扩展了线性时间时态逻辑（LTL），并在多个执行路径上使用连接词进行显式和同时量化，从而使HyperLTL能够表达LTL无法表达的信息流安全策略。给出了一个HyperLTL片段的模型检测算法，并在原型模型检测器中实现了该算法。在HyperLTL中可表达的安全策略类的特征在于超属性的算术层次结构。
2013-07-09 cs.CR cs.LO
The Complexity of Generalized HyperLTL with Stuttering and Contexts
ENS Rennes（雷恩高等师范学院）；Aalborg University（奥尔堡大学）
本文研究了包含停滞和上下文的广义超LTL的可满足性、有限状态可满足性和模型检查问题的复杂性，证明了可满足性为Σ₁¹-完全，而模型检查和有限状态可满足性则等价于二阶算术中的真值，远比可决定的超LTL模型检查问题复杂。
2026-11-02 cs.LO
A Remark on the Expressivity of Asynchronous TeamLTL and HyperLTL
本文研究异步TeamLTL与HyperLTL的表达力关系，证明TeamLTL的布尔析取扩展等价于单全称量词HyperLTL的正布尔闭包，其布尔否定扩展的左向下封闭片段等价于对应布尔闭包。
2024-06-07 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
Non-Deterministic Planning for Hyperproperty Verification
CISPA Helmholtz Center for Information Security（CISPA亥姆霍兹信息安全中心）
本文提出利用非确定性规划作为中间语言，将HyperLTL超属性验证问题转化为QDec-POMDP规划实例，并证明对HyperLTL大片段可归约为经典、FOND或POND规划，实验验证了方法的有效性。
2024-05-22 cs.AI cs.FL cs.LO
