Checking Satisfiability of Hyperproperties using First-Order Logic
本文提出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
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
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
Team Semantics for the Specification and Verification of Hyperproperties
我们开发团队语义的线性时序逻辑（LTL）来表达hyperproperties，这是最近被确定为一个关键的概念，在信息流属性的验证。从概念上讲，我们认为一个异步和同步的团队语义的变体。我们研究了这种新逻辑的基本性质，并对其可满足性、路径和模型检验问题的计算复杂性进行了分类。此外，我们将研究这些基本逻辑的扩展如何对添加其他原子运算符做出反应。最后，我们比较它的表现力的HyperLTL，另一个最近推出的逻辑hyperproperties。我们的研究结果表明，团队语义下的LTL是一个可行的替代HyperLTL，它补充了HyperLTL的表达能力，并具有部分更好的算法性能。
2018-06-25 cs.CC 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
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
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
Deciding Asynchronous Hyperproperties for Recursive Programs
本文提出一种带新机制识别迹位置的异步超性质逻辑，在保持有限状态模型检测复杂度不变且更具表达力的同时，首次为递归程序超性质模型检测提供了合适方法。
2023-10-25 cs.FL cs.LO cs.PL
Second-Order Hyperproperties
本文提出支持对迹集合进行二阶量化的时间逻辑Hyper$^2$LTL，以表达公共知识等复杂超性质，并针对受限片段设计了基于不动点迭代和自动机学习的近似模型检测算法，在工具HySO中验证有效。
2023-05-29 cs.LO
Explainability Requirements as Hyperproperties
本文结合 Lewis 反事实条件句、LTL 与知识模态词形式化多智能体系统的反事实可解释性，并将其嵌入超逻辑，证明模型检测可判定。
2025-10-18 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
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
Deciding branching hyperproperties for real time systems
本文研究实时系统分支超性质的判定问题，提出度量时序逻辑的分支超性质扩展HCMTL*，证明其在时间自动机上的验证不可判定，限定固定时间范围时可通过归约为有界实数域MSO问题实现可判定。
2024-05-20 cs.CR cs.LO
Coinductive Proofs for Temporal Hyperliveness
针对时序超性质演绎证明系统匮乏的问题，提出用共归纳关系近似∀*∃*ψ型超性质，构建Coq中的机械化框架HyCo并验证其可靠性与实用性。
2025-01-14 cs.LO cs.PL
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
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
TAPAAL HyperLTL: A Tool for Checking Hyperproperties of Petri Nets
本文提出了一种针对Petri网的HyperLTL模型检查器，用于验证超属性，该工具集成于TAPAAL框架并展示了其在计算机网络领域的应用性能。
2026-01-09 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
Conformance Relations and Hyperproperties for Doping Detection in Time and Space
本文提出广义掺杂清洁性概念，结合符合性关系与超属性逻辑HyperSTL*，用于时间和空间域上的掺杂检测，并在柴油排放测试案例中验证其有效性。
2022-01-17 cs.LO
Efficient Monitoring of Hyperproperties using Prefix Trees
超属性，如非干扰和观察决定论，将多个计算轨迹相互关联，因此无法通过孤立考虑计算的工具进行监控。我们提出了在最新版本的RVHyper，运行时验证工具hyperproperties的监测方法。该工具的输入是时序逻辑HyperLTL中给出的规范，HyperLTL扩展了具有跟踪量词和跟踪变量的线性时序逻辑（LTL）。RVHyper按顺序处理执行跟踪，直到检测到违反规范。在这种情况下，将返回一组跟踪形式的反例。RVHyper采用了一系列优化：规范的预处理分析和最大限度地减少监控过程中需要存储的跟踪的过程。在这篇文章中，我们介绍了一种新的跟踪存储技术，安排在一个树状结构的痕迹，利用部分相等的痕迹。我们评估RVhyper现有的基准安全信息流控制，纠错码和对称性的硬件设计。作为安全性之外的一个示例应用程序，我们展示了如何使用RVHyper来检测硬件设计中的虚假依赖关系。
2021-01-18 cs.LO
The Hierarchy of Hyperlogics
超性质通过将多个迹联系起来来推广迹的性质，在信息流安全中得到了广泛的研究。最近，已经提出了一些超性质的逻辑，并且需要理解它们的可判定性和相对表达性。新的逻辑已经从标准逻辑中获得了两个主要的扩展：时态逻辑，如LTL和CTL $^*$，已经通过为迹或路径添加变量而被推广到超属性。一阶逻辑和二阶逻辑，如一元一阶序逻辑和MSO，已经用等阶谓词扩展。我们研究了两个扩展的线性时间和分支时间逻辑的频谱的影响，特别是对命题的量化逻辑。由此产生的超逻辑层次结构与经典层次结构有很大不同，这表明等级别谓词比跟踪和路径变量增加了更多的表达能力。在超逻辑的层次结构中，我们确定了可满足性问题的可判定性的新边界。具体来说，我们表明，虽然HyperQPTL和HyperCTL $^*$都是不可判定的一般，公式内的$\exists^*\forall^*$片段是可判定的。
2020-05-12 cs.LO
A Temporal Logic of Security
提出了一种新的安全策略验证逻辑。该逻辑HyperLTL扩展了线性时间时态逻辑（LTL），并在多个执行路径上使用连接词进行显式和同时量化，从而使HyperLTL能够表达LTL无法表达的信息流安全策略。给出了一个HyperLTL片段的模型检测算法，并在原型模型检测器中实现了该算法。在HyperLTL中可表达的安全策略类的特征在于超属性的算术层次结构。
2013-07-09 cs.CR cs.LO
Unifying Asynchronous Logics for Hyperproperties
本文提出 GHyperLTL_SC 超逻辑框架以统一 HyperLTL 的异步扩展与知识逻辑 KLTL，并给出模型检测可判定且表达力更强的 simple 片段。
2024-10-02 cs.LO
On the Complexity of Linear Temporal Logic with Team Semantics
在线性时序逻辑（LTL）中，一个以公式形式给出的规范通过一组迹来定义一个系统。然而，某些功能，如信息流的安全约束，而不是作为所谓的hyperproperties，这是一套套的痕迹。一种逻辑方法是团队逻辑，这是一个逻辑框架，用于规范信息的依赖性和独立性。团队语义的LTL最近被发现是超属性的逻辑。我们研究了具有同步团队语义和布尔否定的LTL的复杂性理论，证明了LTL的模型检验和可满足性问题都是高度不可判定的，等价于三阶算术的判定问题.此外，我们证明，这种复杂性已经出现在小的时间深度和只有“未来”模态F。最后，我们还介绍了口吃不变性的团队语义推广。
2020-04-27 cs.LO
Automata and Fixpoints for Asynchronous Hyperproperties
在过去的十年中，由于它们的重要性，超性质受到越来越多的关注，例如安全分析。过去的方法都集中在同步分析，即技术，其中不同的路径进行比较锁定逐步。本文通过引入一种新的自动机模型（Alternating Asynchronous Parity Automata）和时间不动点演算$\Hmu$，系统地研究了超性质的异步分析.我们表明，这两种模式的表达能力相一致的固定路径分配。这两个模型的高表达能力证明了这样一个事实，即决策问题的利益是高度不可判定的，即，甚至不是算术。作为一种补救措施，我们提出了近似分析这两种模式，也引起自然可判定的片段。
2020-10-22 cs.FL 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
The Complexity of Asynchronous HyperLTL
Aalborg University（奥尔堡大学）
本文研究了异步超属性逻辑AHLTL的模型检测和可满足性问题，证明了模型检测等价于二阶算术真值，而可满足性在轨迹存在量化时为Σ₁¹-完全，在轨迹全称量化时为Σ₁¹-困难且属于Σ₂¹。
2026-10-11 cs.LO
Syntax-Guided Automated Program Repair for Hyperproperties
针对无限状态程序的 HyperLTL 时序超性质，提出结合符号执行、约束生成与 SyGuS 的迭代透明修复方法，以生成贴近原程序行为的补丁，原型实验结果良好。
2024-08-12 cs.LO cs.PL
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
Asynchronous Extensions of HyperLTL
超属性是一种现代规范范式，它扩展了跟踪属性以表达跟踪集的属性。在文献中研究的超属性的时态逻辑，包括HyperLTL，假设一个同步的语义和享受可判定的模型检验问题。在本文中，我们介绍了两个异步和正交扩展的HyperLTL，即口吃HyperLTL（HyperLTLS）和上下文HyperLTL（HyperLTLC）。这两个扩展都很有用，例如，制定信息流安全属性的异步变体。我们表明，对于这些逻辑，模型检验一般是不可判定的。在积极的一面，对于他们中的每一个，我们确定了一个片段与可判定的模型检验，包括HyperLTL，可以表达有意义的异步需求。此外，我们提供了确切的计算复杂性的模型检验这两个片段，HyperLTLS片段，符合严格的表达逻辑HyperLTL。
2021-04-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
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
Realizing Omega-regular Hyperproperties
研究了超逻辑HyperQPTL，它结合了迹关系和$ω$ -正则性的概念.我们证明了HyperQPTL是非常有表现力的，它可以表达诸如不确定性，有界等待授权，认知属性，特别是任何$ω$ -正则属性等属性。这些属性在以前研究过的超逻辑（如HyperLTL）中无法表达。与此同时，我们认为，HyperQPTL的表现力是最佳的，在某种意义上，一个更有表现力的逻辑$ω$ -正则超属性将有一个不可判定的模型检验问题。我们进一步研究了HyperQPTL的可实现性问题。我们证明了可实现性对于包含像不确定性这样的属性的HyperQPTL片段是可判定的。但是，与可满足性问题相比，命题量化确实使超逻辑的可实现性问题更难。更具体地说，具有泛存在命题量词交替后跟单个迹量词的HyperQPTL公式片段通常是不可判定的，即使片段到HyperLTL的投影具有可判定的可实现性问题。最后，我们在原型工具BoSy中实现了HyperQPTL的有界综合问题。使用带有HyperQPTL规范的BoSy，我们已经能够合成几个资源仲裁器。非线性时间超逻辑的综合问题仍然是一个未解决的问题。例如，还不知道如何从分支时间超逻辑（如HyperCTL $^*$）中给出的规范合成系统。
2021-01-18 cs.LO
Verifying Security Policies in Multi-agent Workflows with Loops
我们认为基于Web的工作流，如会议提交系统，如EasyChair的信息流安全策略的自动验证。我们的工作流描述语言允许循环，非确定性的选择，和无限数量的参与代理。信息流策略在超属性的时态逻辑中指定。我们证明了验证问题可以归结为一阶线性时间时序逻辑公式的可满足性，并为相关类别的工作流和规范提供可判定性结果。我们报告的一系列基准上实现我们的方法所获得的实验结果。
2017-08-29 cs.CR 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
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
Logic Column 19: Symbolic Model Checking for Temporal-Epistemic Logics
本文综述了近年来通过符号模型检验验证时态认知逻辑的一些工作，重点介绍了基于OBDD和基于SAT的离散和实时分支时态逻辑的认知逻辑验证方法。
2007-09-04 cs.LO
Logic Column 11: The Finite and the Infinite in Temporal Logic
本文研究了有限和无限序列上的LTL时态算子的解释。这是用来作为一个健全的和完整的公理化的Caret，最近的时间逻辑推理嵌套过程调用和返回的程序推导的基础。
2005-04-24 cs.LO
Epistemic Temporal Logic for Information Flow Security
时间认知逻辑是一个完善的框架，用于表达代理人的知识以及它如何随着时间的推移而演变。在基于语言的安全中，这些是核心问题，例如在解密的情况下。我们建议将这两个领域结合起来。本文提出了一个计算模型和一个认知时态逻辑，用于推理通过观察程序输出获得的知识。这种方法被证明是优雅地捕捉标准的概念，不干扰和解密的文献，以及敏感和公共数据混杂在微妙的方式的信息流属性。
2012-08-30 cs.CR cs.LO cs.MA
Interval Temporal Logic Decision Tree Learning
决策树是一种简单但功能强大的分类模型，用于分类分类和数值数据，尽管简单，但它们通常用于运筹学和管理以及知识挖掘。从逻辑的角度来看，决策树可以看作是用命题逻辑编写的逻辑规则的结构化集合。由于知识挖掘正迅速向时态知识挖掘发展，并且由于在许多情况下时态信息最好由区间时态逻辑描述，因此命题逻辑决策树可能向区间时态逻辑决策树发展。本文定义了区间时态逻辑决策树学习问题，并提出了一种推广经典决策树学习的解决方案。
2020-03-12 cs.LO
Erratum to "Frequency Linear-time Temporal Logic"
我们修正了一个定理的证明，该定理表明频率线性时间时序逻辑的可满足性是不可判定的[TASE 2012]。
2020-10-01 cs.LO
$ω$-Forest Algebras and Temporal Logics
我们使用[4]中介绍的无限树语言的代数框架来导出各种时态逻辑的有效特征，特别是逻辑EF（CTL的一个片段）及其计数变体cEF。
2022-03-25 cs.LO
Complete Intuitionistic Temporal Logics in Topological Dynamics
线性时态逻辑的语言可以在动态拓扑系统类上解释，从而产生了直观时态逻辑${{\sf ITL}^{\sf c}}_{\Diamond,\forall}$，最近Fernán-Duque证明了它是可判定的。在这篇文章中，我们公理化这个逻辑，一些片段，并证明几个熟悉的空间的完备性。
2019-10-02 cs.LO
Systematic Construction of Temporal Logics for Dynamical Systems via Coalgebra
时态逻辑是动态系统的一种明显的高级描述性伴随形式主义，动态系统将行为建模为状态随时间的确定性演化。各种各样的不同的时间逻辑适用于动力系统存在，每个候选人都有自己的实用理由。在这里，提出了一种系统地构建动力系统时态逻辑的方法：首先，注意到动力系统可以以多种方式被视为余代数。其次，一个简单的标准结构的模态逻辑的余代数，即莫斯的余代数逻辑，应用。最后，所得到的系统的特点是相对于他们表达的时间属性。
2012-12-07 cs.LO
A Survey on Temporal Logics
本文综述了广义时态逻辑的主要研究和最新研究，介绍了各种时态逻辑系统，处理了各种时态结构，讨论了时态逻辑的重要特征，如可判定性（或不可判定性）结果、可表达性和证明系统。
2011-04-25 cs.LO
Real-time and Probabilistic Temporal Logics: An Overview
在过去的二十年里，人们对用于描述和验证实时的【形】系统的逻辑形式进行了广泛的研究。时态逻辑一直是这一方向的重要研究课题。虽然许多逻辑已经被引入到实时的【形】和复杂系统的形式化规范，这些逻辑的最新全面的分析并不存在于文献中。在本文中，我们分析实时的【形】和概率时态逻辑已被广泛应用于这一领域。我们外推的概念，可判定性，公理化，表达性，模型检验等，为每个逻辑分析。我们还提供了一个比较的时间逻辑讨论的功能。
2011-04-25 cs.LO
