TAPAAL HyperLTL: A Tool for Checking Hyperproperties of Petri Nets
TU Berlin（柏林工业大学）；Aalborg University（奥尔堡大学）
本文提出了一种针对Petri网的HyperLTL模型检查器，用于验证超属性，该工具集成于TAPAAL框架并展示了其在计算机网络领域的应用性能。
2026-01-09 cs.LO
Logics and Algorithms for Hyperproperties
本文针对需分析多执行路径关系的超性质系统需求，梳理了近十年用于超性质规约的各类逻辑，以及可满足性检查、模型检验等相关算法的研究现状。
2025-01-14 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
On Conformant Planning and Model-Checking of $\exists^*\forall^*$ Hyperproperties
CISPA Helmholtz Center for Information Security, Germany（CISPA海德堡信息安全研究中心）
本文研究了$\exists^*\forall^*$超属性的模型检查与符合计划问题之间的紧密联系，证明两者可以相互转换并建立完整的编码方法。
2025-12-29 cs.AI 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
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
A Temporal Logic for Asynchronous Hyperproperties
超性质是计算系统的性质，其需要多于一个迹来评估，例如，许多信息流安全性和并发性要求。在跟踪属性定义一组跟踪的情况下，超属性定义一组多组跟踪。时态逻辑HyperLTL和HyperCTL* 已经被提出来表达超属性。然而，它们的语义是同步的，因为所有跟踪都以相同的速度进行，并在相同的位置进行评估。这就排除了使用这些逻辑来分析其轨迹可以以不同速度进行的系统，并允许不同的轨迹独立地采取断续步骤。为了解决这个问题，在本文中，我们提出了一个异步变体的HyperLTL。在消极的一面，我们表明，这种变体的模型检查问题是不可判定的。在积极的一面，我们确定了一个可判定的片段，其中涵盖了丰富的公式与实际应用。我们还提出了两个模型检测算法，减少我们的问题的同步语义的HyperLTL模型检测问题。
2021-04-28 cs.LO
Complexity of Model Checking Second-Order Hyperproperties on Finite Structures
CISPA Helmholtz Center for Information Security（CISPA 赫尔姆霍兹信息安全中心）；Bar Ilan University（巴伊兰大学）；Saarland University（萨尔兰大学）
本文研究了超2LTL在有限结构上的模型检查问题，证明其在树状和无环结构上的可判定性，并探讨了不同片段的复杂性。
2026-01-28 cs.FL cs.LO
Temporal Logics for Hyperproperties
提出了两种新的超性质验证逻辑。超属性将安全策略（如不干涉）表征为计算路径集的属性。标准的时态逻辑，如LTL、CTL和CTL*，一次只能引用一条路径，因此不能表达许多感兴趣的超性质。这里提出的逻辑，HyperLTL和HyperCTL*，在多个路径上向LTL和CTL* 添加显式和同时量化。这种量化使得能够表达超性质。给出了该逻辑的模型检验算法。针对HyperLTL的一个片段，实现了一个原型模型检测器。
2014-01-21 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
Probabilistic Hyperproperties with Nondeterminism
我们研究的问题，形式化和检查概率超性质的模型，允许非确定性的行动。我们扩展的时间逻辑\HyperPCTL，这已经介绍了离散时间马尔可夫链，使规范的超性能也马尔可夫决策过程。我们推广HyperPCTL，允许明确和同时量化的随机数和概率计算树，并表明它可以表达重要的定量要求，在安全和隐私。我们发现，HyperPCTL模型检验在MDP是在一般不可判定的量化与记忆的概率概率的排序，但限制域无记忆的非概率排序把模型检验问题可判定。随后，我们提出了一个基于SMT的编码模型检验这种语言，并评估其性能。
2020-07-16 cs.CR cs.FL 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
Statistical Model Checking for Hyperproperties
超属性已被证明是一个强大的工具，用于表达和推理信息流的安全策略。本文研究了超性质的统计模型检验问题。与详尽的模型检验不同，SMC的工作基于从手头的系统中抽取样本，并使用统计置信度评估规范。与穷举技术相比，应用SMC的主要好处是其效率和可扩展性。为了推理概率超属性，我们首先提出了扩展PCTL* 和HyperPCTL的时态逻辑HyperPCLT*。我们表明，HyperPCLT* 可以表达重要的概率信息流的安全策略，不能用HyperPCTL表示。然后，我们介绍了SMC算法验证HyperPCLT* 公式的离散时间马尔可夫链，序列概率比检验（SPRT）的基础上，一个新的概念，多维无差异区域。我们的SMC算法可以处理任何所需的显着性水平的非嵌套和嵌套的概率算子。为了显示我们的技术的有效性，我们评估我们的SMC算法的四个案例研究集中在信息安全：定时侧通道加密的脆弱性，概率匿名用餐密码，概率不干扰并行程序，和性能的随机缓存替换策略，作为一种对策，对缓存刷新攻击。
2020-08-04 cs.CR 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
Probabilistic Hyperproperties of Markov Decision Processes
超属性是将系统的正确性描述为多个执行之间的关系的属性。超属性概括了跟踪属性，包括信息流安全要求，如不干扰，以及对称性、部分观察、鲁棒性和容错等要求。我们开始研究马尔可夫决策过程（MDP）的超性质的规范和验证。我们介绍了时间逻辑PHL（概率超逻辑），它扩展了经典的概率逻辑量化的标记和痕迹。PHL可以表达概率系统的各种超性质，包括经典应用，如概率不干扰，以及机器人和规划等领域的新应用。虽然PHL的模型检验问题一般是不可判定的，我们提供的方法证明和反驳公式的逻辑片段。该片段包括许多感兴趣的概率超性质。
2020-10-13 cs.LO
Deciding Asynchronous Hyperproperties for Recursive Programs
本文提出一种带新机制识别迹位置的异步超性质逻辑，在保持有限状态模型检测复杂度不变且更具表达力的同时，首次为递归程序超性质模型检测提供了合适方法。
2023-10-25 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
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
Asynchronous Extensions of HyperLTL
超属性是一种现代规范范式，它扩展了跟踪属性以表达跟踪集的属性。在文献中研究的超属性的时态逻辑，包括HyperLTL，假设一个同步的语义和享受可判定的模型检验问题。在本文中，我们介绍了两个异步和正交扩展的HyperLTL，即口吃HyperLTL（HyperLTLS）和上下文HyperLTL（HyperLTLC）。这两个扩展都很有用，例如，制定信息流安全属性的异步变体。我们表明，对于这些逻辑，模型检验一般是不可判定的。在积极的一面，对于他们中的每一个，我们确定了一个片段与可判定的模型检验，包括HyperLTL，可以表达有意义的异步需求。此外，我们提供了确切的计算复杂性的模型检验这两个片段，HyperLTLS片段，符合严格的表达逻辑HyperLTL。
2021-04-26 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
The Complexity of Asynchronous HyperLTL
Aalborg University（奥尔堡大学）
本文研究了异步超属性逻辑AHLTL的模型检测和可满足性问题，证明了模型检测等价于二阶算术真值，而可满足性在轨迹存在量化时为Σ₁¹-完全，在轨迹全称量化时为Σ₁¹-困难且属于Σ₂¹。
2026-10-11 cs.LO
The Complexity of Generalized HyperLTL with Stuttering and Contexts
ENS Rennes（雷恩高等师范学院）；Aalborg University（奥尔堡大学）
本文研究了包含停滞和上下文的广义超LTL的可满足性、有限状态可满足性和模型检查问题的复杂性，证明了可满足性为Σ₁¹-完全，而模型检查和有限状态可满足性则等价于二阶算术中的真值，远比可决定的超LTL模型检查问题复杂。
2026-11-02 cs.LO
Visual Analysis of Hyperproperties for Understanding Model Checking Results
模型检查器提供用于证明系统的数学模型满足给定规范的算法。如果发生冲突，则返回一个显示错误行为的反例。理解这些反例是具有挑战性的，特别是对于超属性规范，即，将系统的多个执行相互关联的规范。我们的目标是通过我们的HyperVis工具，它提供了给定的模型，规范和反例的交互式可视化，以促进这种反例的可视化分析。在迭代和跨学科的设计过程中，我们开发了可视化解决方案，可以有效地传达模型检验结果的核心方面。具体来说，我们引入二进制值的图形表示，以提高模式识别，颜色编码，以更好地指示相关方面，视觉增强的文本描述，以及广泛的跨视图突出显示机制。此外，通过对反例的潜在因果分析，我们还能够识别导致违规的值，并将这些知识用于改进编码和突出显示。最后，分析人员可以直接在HyperVis中修改超属性和系统的规范，并启动新版本的模型检验。结合起来，这些特性显著地支持分析人员理解导致反例的错误以及迭代所提供的系统和规范。我们使用HyperVis进行了多个案例研究，并在定性反馈会议中与领域专家进行了测试。参与者的积极反馈证实了与基于文本的手册现状相比的显著改进以及该工具在解释超性质方面的价值。
2021-08-08 cs.HC cs.LO
Unifying Asynchronous Logics for Hyperproperties
本文提出 GHyperLTL_SC 超逻辑框架以统一 HyperLTL 的异步扩展与知识逻辑 KLTL，并给出模型检测可判定且表达力更强的 simple 片段。
2024-10-02 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
Verifying Asynchronous Hyperproperties in Reactive Systems
CISPA Helmholtz Center for Information Security（CISPA亥姆霍兹信息安全中心）
本文提出了一种基于游戏的方法，用于验证反应系统中任意∀*∃* A-HLTL公式，解决了异步超属性的模型检查问题。
2025-12-29 cs.FL 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
The Complexity of Generalized HyperLTL with Stuttering and Contexts
本文确定了带 stuttering 和 contexts 的广义 HyperLTL 的可满足性与模型检测复杂度，证明可满足性为 $Σ_1^1$-完全，而模型检测等价于二阶算术真值且远难于 HyperLTL。
2025-09-17 cs.FL cs.LO
HyperQB: A Bounded Model Checker for Hyperproperties
Michigan State University（密歇根州立大学）；IMDEA Software Institute（IMDEA软件研究所）
本文提出 HyperQB 2.0，一个面向 HyperLTL/A-HLTL 超性质的一键式有界模型检查器，结合 SMT 与 QBF 支持有限及无限状态程序验证。
2025-10-21 cs.CR cs.LO
AutoHyper: Explicit-State Model Checking for HyperLTL
HyperLTL是一种可以表达超属性的时态逻辑，即，与系统的多个执行跟踪相关的属性。这样的性质变得越来越重要并且自然发生，例如，在信息流控制，鲁棒性，突变测试，路径规划和因果关系检查。到目前为止，HyperLTL的完整模型检验工具仅限于无替代公式，即，仅使用泛量化或仅使用存在迹量化的公式。涉及量词替换的属性只能以不完整的方式处理，即，即使该属性保持，验证也可能失败。在本文中，我们提出了AutoHyper，一个显式状态自动机为基础的模型检查器，支持完整的HyperLTL，并完成与任意量词交替的属性。我们表明，语言包含检查可以集成到HyperLTL验证，这使得AutoHyper受益于一系列现有的包含检查工具。我们评估AutoHyper的一组广泛的基准来自不同领域的文献，并将其与现有的（不完整的）方法进行HyperLTL验证。
2023-01-26 cs.LO
Temporal Team Semantics Revisited
本文提出基于时间评估函数的时间团队语义学，用于规范异步超属性，并证明同步TeamLTL的嵌入、某些TeamCTL片段MC的高度不可判定性，以及TeamCTL*到交替异步Büchi自动机的翻译及可判定性结果。
2024-02-05 cs.CC cs.LO
Space-Efficient Bounded Model Checking
现有的有界模型检验算法使用SAT方法来检验布尔公式的可满足性。这些方法遭受潜在的内存爆炸问题。基于量化布尔公式（QBF）的有效性的方法允许检查公式的指数更简洁的表示，因为不需要“展开”的过渡关系。由于缺乏一个有效的QBF决策过程，这些方法没有得到广泛的应用。我们评估使用QBF有界模型检验（BMC），使用通用SAT和QBF求解器。我们开发了一个特殊用途的决策过程中使用的BMC QBF，并比较我们的技术与使用通用SAT和QBF求解器在现实生活中的工业基准的方法。
2007-10-25 cs.LO
Bounded Model Checking of an MITL Fragment for Timed Automata
时间自动机（TA）是一种常见的建模时间系统的形式。有界模型检验（BMC）是一种使用SAT或SMT求解器搜索违反属性的运行的验证方法。MITL是线性时间逻辑LTL的实时扩展。最初，MITL被定义为非重叠时间间隔的轨迹，而不是“超密集”时间轨迹，允许时间间隔重叠在单个点上，这些点被当今常见的时间自动机语义所采用。在本文中，我们扩展的MITL片段的语义超密集的时间轨迹，并设计了一个有界的模型检验编码的片段。我们证明了正确性和完整性的意义上说，使用一个足够大的范围内的反例，任何给定的非控股property.We可以找到实现建议的有界模型检验方法和实验研究的效率和可扩展性的实现。
2013-04-26 cs.LO
Integrating Loop Acceleration into Bounded Model Checking
本文将循环加速技术动态集成到基于SMT的有界模型检测中，通过添加捷径和阻塞子句，既能快速发现深层反例，又能在BMC发散时证明安全性，实验表明其在证明不安全性方面具有竞争力。
2024-08-09 cs.LO
Scaling Bounded Model Checking By Transforming Programs With Arrays
有界模型检验是发现程序缺陷最成功的技术之一。然而，模型检查器是资源饥渴，往往无法验证程序循环迭代在大型arrays.We提出了一个转换，使有界模型检查器验证某一类数组属性。我们的技术将数组操作（ANSI-C）程序转换为无数组和无循环（ANSI-C）程序，从而显着降低了模型检查器的资源需求。转换后的程序的模型检验使用现成的有界模型检验器有效地模拟循环迭代。因此，我们的转换程序是一个健全的抽象的原始程序，也是精确的，在大量的情况下-我们正式的类的程序，它保证是精确的。我们在行业规范和学术基准上证明了我们的技术的适用性和有用性。
2017-03-07 cs.LO
Functional Reduction to Speed Up Bounded Model Checking
Hong Kong University of Science and Technology (Guangzhou)（香港科技大学（广州））
FRAIG-BMC通过功能简化减少冗余，提升边界模型检查的效率和性能。
2025-12-07 cs.LO
Model Checking Resource Bounded Systems with Shared Resources via Alternating Büchi Pushdown Systems
资源受限的多智能体系统的验证一般是不可判定的。在许多这样的设置中，资源对于代理是私有的。本文研究了基于交替时序逻辑（ATL）的资源逻辑在共享资源下的模型检验问题。资源可以被消耗和生产到任何数量。我们表明，模型检验问题是不可判定的，如果两个或两个以上的这样的无界资源。我们的主要技术成果是，在一个单一的共享资源的情况下，问题变得可判定。虽然直观，可判定性的证明是不平凡的。我们减少模型检验的问题交替Büchi下推系统。一个中间结果连接到一般的基于自动机的验证：我们表明，模型检验计算树逻辑（CTL）（紧凑）交替Büchi下推系统是可判定的。
2015-08-14 cs.LO
Forward Analysis and Model Checking for Trace Bounded WSTS
我们研究了良结构变迁系统（WSTS）的一个子类，即Ginsburg和Spanier（trans. AMS 1964）意义下的有界完全确定性系统，我们认为它为Finkel和Goubault-Larrecq（Logic. Meth. Comput. Sci. 2012年）。事实上，我们证明，不同于其他条件考虑以前终止的前向分析，有界性是可判定的。有界性被证明是一个有价值的限制WSTS验证，因为我们表明，它进一步允许决定所有的$ω$ -经常属性的无限的痕迹的系统。
2016-03-04 cs.LO
The parameterized space complexity of model-checking bounded variable first-order logic
本文研究有界变量一阶查询模型检测的参数化空间复杂度，建立树层次结构完备性，提出高空间效率检测器，并探讨其最优性。
2019-09-19 cs.LO
Bounded Model Checking for Unbounded Client Server Systems
IIT Dharwad（印度理工学院达瓦德分校）；NIT Calicut（卡尔库特国立理工学院）
本文提出了一种新的计数逻辑和二维有界模型检查策略，用于验证具有无限客户端的客户端-服务器系统。
2026-02-18 cs.LO
Verifying Hyperliveness
HyperLTL是线性时间时态逻辑的扩展，用于规范超属性，即，与多个计算轨迹相关的时间属性。HyperLTL可以表达信息流策略以及互斥算法中的对称性或抗错误传输协议中的汉明距离等属性。以前的工作对HyperLTL模型检验的重点是替代自由片段的HyperLTL，其中验证减少到检查一个标准的跟踪属性在一个适当的自我组成的系统。然而，无替代片段并不涵盖一般的超活性属性。例如，通用公式不能表达保密要求，即对于秘密变量的每一个可能值，都存在一个计算，其中值是不同的，而外部观察者所做的观察是相同的。在本文中，我们研究了更困难的情况下，hyperliveness属性表示为HyperLTL公式与量词交替。我们减少存在量化的战略选择，并表明合成算法可以用来消除存在量词自动。我们还表明，这种方法可以扩展到反应系统的合成，即，自动构建一个反应系统，保证满足给定的HyperLTL公式。
2020-05-15 cs.LO
FO model checking of geometric graphs
在过去的二十年里，一阶（FO）模型检验算法的研究主要集中在稀疏关系结构上--最终由Grohe、Kreutzer和Siebertz提出的FPT算法，用于对无处密集的图类进行FO模型检验。与此相反，除了局部有界的顶点宽度的情况下，只有很少的是目前所知的密集类的图或其他结构的FO模型检验。我们研究的FO模型检验问题的稠密图类定义的几何手段（相交和可见性图）。我们得到新的非平凡FPT结果，例如，对于圆弧、圆、盒、盘和双可见性图的受限子类。这些结果使用FPT算法Gajarskeleton等人。有界宽度偏序集的FO模型检验。我们还通过相关的硬度降低来补充易处理性结果。
2018-03-26 cs.LO
Efficient Algorithms for Time- and Cost-Bounded Probabilistic Model Checking
在概率定时系统的设计中，关于在给定时间、能量或更一般的成本预算内发生的行为的有界要求是至关重要的。传统上，这样的需求已经通过根据成本约束展开模型来减少到无界情况来进行模型检查。这加剧了状态空间爆炸问题，并显著增加了运行时间。在本文中，我们提出了三个新的算法来模型检查的时间和成本有界的马尔可夫决策过程和概率时间自动机，避免展开的属性。它们是基于一个修改的值迭代过程，枚举的状态，并消除技术。我们现在可以得到结果的任何成本限制在一个单一的状态空间不大于相应的无界或期望值属性。特别是，我们可以自然地计算累积分布函数，而无需开销。我们评估的适用性，并比较我们的新算法的性能和他们的实施从文献中的一些案例研究。
2016-05-18 cs.LO
Linear Encodings of Bounded LTL Model Checking
研究线性时序逻辑的有界模型检验问题。我们提出了几个有效的编码，具有大小线性的界限。此外，我们展示了如何编码可以扩展到LTL与过去的运营商（PLTL）。广义编码仍然是线性的大小，但不能检测最小长度的反例。通过使用虚拟展开技术可以捕获最小长度的反例，然而，在规范中编码的大小是二次的。我们还扩展虚拟展开的Buchi自动机，使他们能够接受最小长度的反例。我们的BMC编码可以是增量的，以便从增量SAT技术中受益。通过相当小的修改，增量编码可以通过终止检查进一步增强，允许我们使用BMC证明属性。实验清楚地表明，我们的新编码大大提高了BMC的性能，特别是在增量编码的情况下，并且它们在发现错误方面非常有竞争力。对活性到安全性转换的分析揭示了本文中BMC编码的许多相似之处。使用基于BDD的不变式检查的活性到安全性的转换结果在一个有效的方法来找到最短的反例，补充基于BMC的方法。
2006-11-16 cs.LO
Type-checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion
我们提出了第一个会话类型系统，保证可能非终止通信进程的请求-响应活性属性。这些类型用一组所需的响应来扩充标准二进制会话类型的分支和选择类型，这表明每当选择特定标签时，最终也必须选择一组其他标签，即其响应。我们证明，这些扩展类型是严格的表达比标准的会话类型。我们提供了一个类型系统的过程演算类似于一个子集的内部（基于数据）和外部（基于事件）分支，消息传递，有界和无界循环的协作BPMN流程。我们证明了这个类型系统是合理的，即，它保证了无死锁进程的请求-响应活性。我们在一个无限状态系统的具体例子上说明了微积分和类型系统的使用。
2016-01-05 cs.LO
Constraint LTL Satisfiability Checking without Automata
本文提出了一种新的方法来判定用线性时态逻辑语言写的带有将来和过去算子的公式和属于约束系统D的原子公式的可满足性（简称CLTLB（D））。该技术基于有界可满足性的概念，并将CLTLB（D）公式编码为QF-EUD，结合了无量词等式理论和D.类似于标准LTL，其中有界模型检查和SAT求解器可以用作自动机理论方法的模型检查的替代方案，我们的方法允许用户通过SMT求解技术来解决CLTLB（D）公式的可满足性问题，而不是通过检查合适的自动机A_A的语言的空性。该技术是有效的，并已在我们的Zot形式化验证工具中实现。
2014-02-11 cs.LO
Improved Bounded Model Checking of Timed Automata
时间自动机（TA）是一个非常流行的建模形式主义的时间敏感的属性。一个常见的任务是验证TA的网络是否满足给定的属性，通常用线性时态逻辑（LTL）或时间计算树逻辑（TCTL）的子集表示。在本文中，我们建立在TACK有界模型检查TA，它支持基于信号的语义TA和更丰富的度量区间时态逻辑（MITL）。TACK将TA网络和属性编码为LTL的变体，即时钟约束LTL（CLTLoc）。产生的CLTLoc公式然后可以通过诸如Zot的工具求解，该工具将CLTLoc属性转换为可满足性模理论（SMT）求解器的输入逻辑。我们提出了一种新的方法，保留TACK的MITL属性的编码，同时直接到SMT求解器语言编码的TA网络，利用BitVector逻辑和逻辑的实算术。我们还介绍了几个优化，使我们能够显着优于CLTLoc编码在许多实际情况下。
2021-04-26 cs.LO
Model-Checking for Successor-Invariant First-Order Formulas on Graph Classes of Bounded Expansion
本文证明在后继不变一阶公式的模型检测问题上，当底层 Gaifman 图类具有有界扩张时该问题是固定参数可解的，从而推广了此前关于平面图、排除固定子式等图类的结果。
2017-05-21 cs.LO
Bounded Model Checking of Temporal Formulas with Alloy
Alloy是一种基于一阶关系逻辑的形式化建模语言，它不支持指定反应式系统。我们建议使用时序逻辑来指定这样的系统，并显示如何有界模型检验可以与合金分析仪进行。
2015-06-25 cs.LO cs.SE
A Tree-Shaped Tableau for Checking the Satisfiability of Signal Temporal Logic with Bounded Temporal Operators
Politecnico di Milano（米兰理工大学）；TU Wien（维也纳工业大学）
针对信息物理系统中带界时间算子的离散时间信号时序逻辑（STL）的可满足性检验需求，提出一种利用时间区间冗余加速的树形单次表算法，可拓展用于多种STL相关验证任务，性能优于现有最优编码方法。
2025-07-29 cs.LO
On-the-fly Fast Mean-Field Model-Checking: Extended Version
一种新的，可扩展的，在飞行模型检验程序，以验证有界的PCTL属性的背景下，非常大的系统中的独立的相互作用的对象。该方法结合了动态模型检验技术和离散时间的确定性平均场近似。的渐进正确性的程序和一些结果的应用程序的原型实现的FlyFast模型检测器。
2013-12-12 cs.LO
Bounded LTL Model Checking with Stable Models
本文介绍了异步并发系统的有界模型检验，作为回答集编程的一个很有前途的应用领域。作为异步系统的通信自动机，1-安全Petri网的推广模型，使用。它示出了如何1-安全的Petri网和对网络的行为的要求可以被翻译成一个逻辑程序，这样的有界模型检验问题的网可以通过计算相应的程序的稳定模型来解决。稳定模型语义的使用导致有界可达性和死锁检测任务的紧凑编码，以及线性时序逻辑的有界模型检验的更一般的问题。给出了所设计的翻译的正确性证明，并给出了使用该翻译和Smodels系统的一些实验结果。
2003-05-23 cs.AI cs.LO
