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 of Temporal Formulas with Alloy
Alloy是一种基于一阶关系逻辑的形式化建模语言，它不支持指定反应式系统。我们建议使用时序逻辑来指定这样的系统，并显示如何有界模型检验可以与合金分析仪进行。
2015-06-25 cs.LO cs.SE
Bounded Model Checking for Unbounded Client Server Systems
IIT Dharwad（印度理工学院达瓦德分校）；NIT Calicut（卡尔库特国立理工学院）
本文提出了一种新的计数逻辑和二维有界模型检查策略，用于验证具有无限客户端的客户端-服务器系统。
2026-02-18 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
Bounded LTL Model Checking with Stable Models
本文介绍了异步并发系统的有界模型检验，作为回答集编程的一个很有前途的应用领域。作为异步系统的通信自动机，1-安全Petri网的推广模型，使用。它示出了如何1-安全的Petri网和对网络的行为的要求可以被翻译成一个逻辑程序，这样的有界模型检验问题的网可以通过计算相应的程序的稳定模型来解决。稳定模型语义的使用导致有界可达性和死锁检测任务的紧凑编码，以及线性时序逻辑的有界模型检验的更一般的问题。给出了所设计的翻译的正确性证明，并给出了使用该翻译和Smodels系统的一些实验结果。
2003-05-23 cs.AI 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
A Metric Encoding for Bounded Model Checking (extended version)
在有界模型检验中，系统模型和被检验的属性都被转换成一个布尔公式，由SAT求解器进行分析。我们介绍了一种新的编码技术，这是特别优化的管理定量未来和过去的度量时间运营商，通常发现在硬实时的系统的属性。编码是简单和直观的原则上，但它是更复杂的存在下，典型的有界模型检验技术，向后和向前的循环用于表示一个最终的周期性无限域的有限结构。我们报告和评论的新的编码技术，并进行了广泛的实验，以评估其可行性和有效性。
2009-07-27 cs.LO cs.SE
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
A Note on the Complexity of Model-Checking Bounded Multi-Pushdown Systems
本文给出了模型检验多下推系统的复杂性刻画。多下推系统对递归并发程序进行建模，其中任何顺序进程都具有有限控制。我们认为有界性的三个标准概念：上下文有界性，相位有界性和堆栈排序。逻辑形式主义是一个线性时间时态逻辑，扩展了著名的逻辑CaRet，但专用于多下推系统，其中抽象运算符（与调用和返回有关），例如下一次和直到被堆栈参数化。我们表明，这个问题是EXPTIME-完全的上下文有界的运行和一元编码的上下文开关的数量，我们还证明了这个问题是2 EXPTIME-完全的相位有界的运行和一元编码的相位开关的数量。在这两种情况下，值k都作为输入给出（因此它不是模型检验问题的常数），这在复杂性上产生了实质性的差异。在某些情况下，我们的结果改善了以前的复杂性结果。
2012-12-06 cs.FL cs.LO
Technical Report: Model-Checking for Resource-Bounded ATL with Production and Consumption of Resources
文献中已经提出并研究了几种表示资源约束下联盟能力的逻辑。已有的工作表明，如果只考虑资源的消耗，或者系统中任意路径上产生或消耗的资源总量是有界的，那么几种标准逻辑（如资源有界联合逻辑（RB-CL）和资源有界交替时序逻辑（RB-ATL））的模型检验问题是可判定的.然而，对于具有无限资源生产和消费的联盟逻辑，只知道一些不可判定性结果。本文证明了资源无限生产和无限消耗的RB-ATL的模型检验问题是可判定的，但是EXPSPACE困难的.我们还调查了一些易于处理的情况下，并提供了一个详细的比较，资源逻辑RAL的一个变种，连同新的复杂性结果。
2015-04-25 cs.LO cs.MA
Type-checking Liveness for Collaborative Processes with Bounded and Unbounded Recursion
我们提出了第一个会话类型系统，保证可能非终止通信进程的请求-响应活性属性。这些类型用一组所需的响应来扩充标准二进制会话类型的分支和选择类型，这表明每当选择特定标签时，最终也必须选择一组其他标签，即其响应。我们证明，这些扩展类型是严格的表达比标准的会话类型。我们提供了一个类型系统的过程演算类似于一个子集的内部（基于数据）和外部（基于事件）分支，消息传递，有界和无界循环的协作BPMN流程。我们证明了这个类型系统是合理的，即，它保证了无死锁进程的请求-响应活性。我们在一个无限状态系统的具体例子上说明了微积分和类型系统的使用。
2016-01-05 cs.LO
FO Model Checking on Posets of Bounded Width
在过去的二十年中，研究一阶（FO）模型检验算法的主要焦点一直是稀疏关系结构-最终由Grohe，Kreutzer和Siebertz提出的FPT算法，用于对无处密集的图类进行FO模型检验[STOC'14]，密集结构最近才开始引起人们的注意。Bova，Ganian和Szeider [LICS'14]发起了对偏序集（偏序集）上FO模型检验复杂性的研究。Bova、Ganian和Szeider证明了模型检验存在FO逻辑在有界宽度的偏序集上是固定参数可处理的（FPT），其中偏序集的宽度是偏序集中最大反链的大小。然而，对于有界宽度偏序集上的一般FO模型检验，FPT算法的存在性仍然是开放的。我们给出了一个算法，它以宽度为$w$的$n$元偏序集$\cal P$和FO逻辑公式$ϕ$为输入，判定$ϕ$在时间$f(ϕ,w)\cdot n^2$上是否在$\cal P$上成立.
2015-05-29 cs.DM 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
On Distributed Model Checking of MSO on Graphs
我们认为分布式模型检查的一元二阶逻辑（MSO）的图构成的通信网络的拓扑结构。因此，图既是被检查的结构，也是执行分布式计算的系统。我们证明了MSO可以分布式模型检查，只有一个常数的消息发送到每个链接的平面网络有界直径，以及网络有界度和有界树长。分布式算法依赖于非平凡变换的线性时间顺序算法有界树宽图的树分解。
2009-04-13 cs.DC cs.LO
Bounded Model Checking of C++ Programs Based on the Qt Framework (extended version)
嵌入式系统的软件开发过程越来越快，这通常会导致相关复杂性的增加。因此，消费电子公司通常在快速和自动验证过程中投入大量资源，以创建强大的系统并降低产品召回率。正因为如此，本文提出了一个简化版本的Qt框架，这是集成到有效的基于SMT的有界模型检验工具，以验证实际应用程序，使用所提到的框架。本文提出的方法提出了一个成功率为94.45%，为开发的测试套件。
2015-09-05 cs.LO cs.SE
Model Checking on Interpretations of Classes of Bounded Local Cliquewidth
本文提出了一种固定参数的一阶模型检验算法，用于对局部宽度有界的图类进行解释。值得注意的是，这包括平面图的解释，更一般地，有界亏格的类。为了获得这一结果，我们开发了一种新的工具，它适用于一个非常一般的设置依赖类，我们相信这可以是一个重要的组成部分，在未来实现类似的结果。
2022-02-25 cs.DM cs.DS cs.LO
Scaling Bounded Model Checking By Transforming Programs With Arrays
有界模型检验是发现程序缺陷最成功的技术之一。然而，对于在大型数组上进行循环迭代的程序，有界模型检查器通常会超出其可用资源的限制。我们提出了一个转换，使有界模型检查器，以验证某一类数组属性。我们的技术将ANSI-C中的数组操作程序转换为无数组和无循环的程序。转换后的程序可以有效地验证一个现成的有界模型检查。虽然变换后的程序是，在一般情况下，原程序的抽象，我们正式表征的性质，变换是精确的。我们在行业规范和学术基准上证明了我们的技术的适用性和有用性。
2016-08-17 cs.LO cs.PL
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
Using Bounded Model Checking to Focus Fixpoint Iterations
在通过抽象解释的静态分析中，两个经典的不精确性来源是加宽和合并操作。合并操作可以通过区分路径来完成，就像在跟踪分区中一样，代价是枚举指数数量的路径。在这篇文章中，我们描述了如何避免这种系统的探索，集中在一个单一的路径，指定的SMT解决。我们的方法与加速技术结合得很好，因此在某些情况下也可以消除加宽。我们说明了它的公知的凸多面体域。
2011-06-14 cs.LO cs.PL
From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques
我们提出了一个有界等价性验证技术的高阶程序与局部状态。该技术结合了完全抽象的符号环境互模拟类似的符号游戏语义，新的技术，轻量级的状态不变的注释。这产生了没有假阳性或假阴性的等效性验证技术。该技术是有界完备的，因为所有的不等式都是自动检测到足够大的界限。此外，几个硬等价证明自动或后被注释与状态不变量。我们在一个名为Hobbit的工具原型中实现了该技术，并使用一组广泛的新的和现有的示例对其进行基准测试。霍比特人可以证明许多经典的等价关系，包括所有迈耶和西伯的例子。
2021-10-22 cs.LO cs.PL
Fly-automata for checking MSO 2 graph properties
一个描述性更强但太长的标题是：构造飞行自动机来检查用边量化写的一元二阶公式表示的有界树宽图的性质。这些特性简称为MSO 2。Fly-automata（FA）在表示图的术语上自底向上运行，并“动态”计算必要的状态和转换，而不是查看巨大的，实际上无法实现的表。在以前的工作中，我们已经构造了处理表示有界宽度的图的项的FA，以检查它们的一元二阶（MSO）性质（由没有边量化的公式表示）。在这里，我们适应这些FA的关联图，使他们可以检查MSO 2属性的有界树宽度的图。这是可能的，因为：（1）图的MSO ~ 2性质就是图的关联图的MSO性质;（2）图的关联图的树宽是线性有界的。我们的结构实际上是可实现的和可用的。我们详细介绍了具体的结构自动机在这个角度来看。
2015-12-22 cs.LO
Bounded Model Checking of Pointer Programs Revisited
指针程序的有界模型检验是一种调试技术，用于操作堆上动态分配的指针结构的程序。它基于以下四点意见。第一，错误条件（如悬空指针的解引用）可以用双变量一阶逻辑的~片段来表示。其次，片段在最弱的前提条件wrt下是封闭的。有限路径第三，数据结构，如树、列表等，可以通过在数据库片段中定义的归纳谓词来表达。最后，双变量逻辑和数据库的两个片段的组合是可判定的。在本文中，我们通过扩展底层逻辑的表达能力来改进这种技术。在~序列的例子中，我们证明了新的逻辑是能够建模更复杂的数据结构与更复杂的依赖堆和更复杂的分析。
2016-02-29 cs.LO cs.PL
Proving Safety with Trace Automata and Bounded Model Checking
循环欠近似是一种技术，它通过额外的分支来丰富C程序，这些分支代表了（有限的）循环迭代范围的效果。虽然这种技术可以显著地加速错误的检测，但它引入了冗余的执行跟踪，这可能使程序的验证复杂化。这对于基于有界模型检验的验证工具尤其如此，该工具结合了简化的算法来确定是否已经考虑了循环的所有可行迭代。我们提出了一种技术，使用\emph{trace automata}，以消除执行循环加速后的冗余执行。该方法减小了分析下的程序的直径，这在某些情况下足以允许使用有界模型检验的安全性证明。我们的转换是精确的-它不会引入假阳性，也不会掩盖任何错误。我们已经实现了分析作为一个源到源的转换，并提出了实验结果显示该技术的适用性。
2014-10-21 cs.FL cs.LO cs.PL
Bounded Model Checking of Max-Plus Linear Systems via Predicate Abstractions
本文介绍了最大线性系统的谓词抽象。从系统矩阵以及所考虑的规范中自动选择等同器械。我们专注于验证时间差规格，其中包括连续事件之间的关系MPL系统。我们实现了一个有界的模型检验（BMC）过程中的谓词抽象的给定MPL系统，以验证时间差规格的满意度。我们的谓词抽象实验表明，改善现有的MPL抽象算法。此外，重点是BMC算法，我们可以提供一个明确的上限的完整性阈值的瞬态和底层MPL系统的循环。
2019-07-08 cs.LO cs.SY eess.SY
SAT-based Explicit LTLf Satisfiability Checking
我们在这里提出了一个基于SAT的框架LTLf（有限迹上的线性时态逻辑）可满足性检查。我们使用命题SAT解决技术来构建一个过渡系统的输入LTLf公式，可满足性检查，然后减少到一个路径搜索问题，在这个过渡系统。此外，我们引入CDLSC（可满足性检查驱动的LTLf），一种新的算法，利用命题SAT求解器从满足性和不满足性结果产生的信息。实验评估表明，CDLSC优于所有其他现有的方法LTLf可满足性检查，通过展示一个近似四倍的加速比第二最好的求解器。
2018-11-07 cs.LO
JBMC: A Bounded Model Checking Tool for Java Bytecode
JBMC是一个开源的基于SAT和SMT的有界模型检验工具，用于验证Java字节码。JBMC依赖于Java库的操作模型，它保守地近似于它们的语义，以验证断言违规，数组越界，意外的算术溢出以及Java字节码中的其他类型的功能和运行时错误。如果状态空间的深度上界是已知的，则JBMC可以用于伪造属性或证明程序正确性。JBMC的实际应用包括但不限于错误发现、属性检查、测试输入生成、安全漏洞检测和程序合成。在这里，我们提供了一个详细的描述JBMC的架构和它的功能，包括深入讨论其背景理论和底层技术，包括一个国家的最先进的字符串求解器，以确保Java字节码的安全性和安全性。
2023-02-05 cs.LO cs.PL cs.SE
Checking Timed Bisimulation with Bounded Zone-History Graphs -- Technical Report
时间自动机（TA）是一个行之有效的形式化描述离散状态/连续时间行为的时间临界反应系统。关于基本分析问题的候选人的实现对规范进行比较，都给定为TA，它已被证明，定时跟踪等价是不可判定的，而定时互模拟等价是可判定的。相应的证明利用区域图，一个有限的，但通常非常占用空间的TA语义表征。因此，大多数实用的TA工具利用区域图，而不是符号和一般更有效的表示TA语义，自动化分析任务。然而，区域图只产生声音的分析任务的结果被简化为平原可达性问题，从而检查定时双相似性太不精确。在本文中，我们提出了有界区域历史图，一种新的表征TA语义促进可调的权衡精度和可扩展性之间的时间双相似性检查。据我们所知，我们的工具TimBrCheck是目前唯一可用的工具，用于有效地检查定时双相似性，甚至支持无声移动的非确定性TA。我们进一步提出了实验结果，从应用我们的工具收集的社区基准，提供洞察精度和效率之间的权衡，取决于绑定值。
2020-09-16 cs.FL cs.LO
Compact Labelings For Efficient First-Order Model-Checking
我们考虑可以从标签检查的图形属性，即，位序列，对数长度附加到顶点。我们证明了存在这样一个标签检查一个一阶公式的自由集变量在图的每一个类是\emph{nicely locally cwd-decomposable}。这个概念概括了\emph{nicely locally tree-decomposable}类的概念。这些类的图可以由具有有限重叠的有界\emph{clique-width}的图覆盖。我们也考虑这样的标签的\emph{bounded}一阶公式的图形类的\emph{bounded expansion}。其中一些结果被扩展到计数查询。
2014-07-08 cs.DS cs.LO
Verifying Fixed-Point Digital Filters using SMT-Based Bounded Model Checking
在基于定点运算的处理器中实现数字滤波器会导致与有限字长相关的问题。特别地，在这样的滤波器中的信号的处理可以产生由在累加加法和乘法运算期间的量化和舍入效应引起的溢出和不想要的噪声。在本文中，我们描述了一种新的方法来验证数字滤波器使用现成的有界模型检查器称为ESBMC，它支持完整的C/C++，是基于可满足性模理论求解器。特别是，我们能够验证溢出的发生，极限环，和时间约束的基础上实现的离散时间模型在C。实验表明，该方法可以用来验证数字滤波器定点实现中的潜在问题，从而可以有效地发现现实的设计错误。
2013-07-23 cs.LO cs.SE
Fault Localization in Multi-Threaded C Programs using Bounded Model Checking (extended version)
软件调试是一个非常耗时的过程，对于多线程程序来说，由于线程调度算法的不确定性行为，这一过程甚至更糟。然而，如果使用自动方法来定位故障，则可以大大减少调试时间。在这项研究中，提出了一种新的方法，故障定位，在多线程的C程序。它将多线程程序转换为相应的顺序程序，然后使用适合于这类程序的故障诊断方法，以定位故障。代码转换是用来自反例的规则和上下文切换信息实现的，反例通常由有界模型检查器生成。实验结果表明，该方法是有效的，在这样一种方式，顺序故障定位方法可以扩展到多线程程序。
2015-09-08 cs.LO cs.SE
Model Checking Existential Logic on Partially Ordered Sets
我们研究了在有限偏序集（简称偏序集）中检验存在句（即使用存在量词和所有布尔连接词构建的前缀形式的一阶句）是否为真的问题。偏序集是一个自反的、反对称的、传递的有向图。这个问题包括基本的嵌入问题，找到一个同构的副本偏序集作为诱导子结构的另一个偏序集。模型检验存在逻辑已经是NP-困难的固定偏序集，因此，我们研究的结构性质的偏序集产生条件的固定参数易处理的问题时，参数化的句子。我们确定宽度作为一个中心的结构属性（偏序集的宽度是成对的不可比元素的子集的最大大小），我们的主要算法的结果是，模型检验存在逻辑类的有限偏序集的有界宽度是固定参数听话。我们观察到一个类似的现象，在经典的复杂性，我们证明了同构问题是多项式时间有界宽度的偏序集类听话，这解决了一个开放的问题，为了理论。我们围绕我们的主要算法结果的复杂性结果限制较少，自然相邻类的有限偏序集，在这个意义上建立其紧密性。我们还将我们的工作与（并证明其独立性）的基本固定参数的有界度和有界宽度的有向图的模型检验的易处理性结果。
2014-04-15 cs.DS cs.LO
Model checking Branching-Time Properties of Multi-Pushdown Systems is Hard
我们解决了多下推系统的共享内存并发程序的模型检验问题。我们认为在这里布尔程序与有限数量的线程和递归过程。众所周知，这类程序的模型检验问题是不可判定的。在本文中，我们调查的可判定性和这个问题的复杂性的假设下，有界的上下文切换定义的Qadeer和Zeroof，和相位有界的La Torre等人提出的。对时间逻辑，特别是分支时间逻辑，如模态$μ$ -演算或CTL的模型检验这样的系统很少受到关注。众所周知，与模态$μ$ -演算密切相关的奇偶博弈对于有界相位系统类是可判定的（因此对于有界上下文切换也是如此），但具有非初等复杂性（赛斯）。一个自然的问题是，这种高复杂性是否是不可避免的，有什么方法来绕过它。本文解决这些问题，不幸的是，有点令人惊讶的是，它表明，分支模型检验的MPDS本质上是一个很难的问题，没有简单的解决方案。我们证明了在相位限制下的MPDS上的奇偶博弈是非初等的。我们的主要结果表明，模型检验的$k$上下文有界MPDS对一个简单的CTL片段，由公式，其时间运营商来自集合${\EF, \EX}$，有一个非初等的下界。
2012-05-31 cs.FL cs.GT cs.LO
Complexity of Model Checking for Modal Dependence Logic
模态依赖逻辑（Modal Dependence Logic，MDL）是由Väänänen最近提出的。它通过操作符=（）增强了基本模态语言。对于命题变量p_1，.，p_n原子式=（p_1，...，p_（n-1），p_n）直观地说明p_n的值仅由p_1，.，p_（n-1）。我们证明了Kripke结构上MDL公式的模型检验是NP完全的，并进一步考虑了通过限制允许的命题和模态连接词的集合而得到的MDL片段。事实证明，几个片段，例如，没有情态动词或没有命题连接词的句子仍然是NP完全的。我们还考虑了MDL的限制，其中每个单个依赖原子的长度由整个逻辑固定的数字限制。我们表明，这个有界MDL的模型检验问题仍然是NP完全的。我们还通过允许经典析取（由Sevenster引入）来扩展MDL，除了依赖析取之外，并表明经典析取总是至少与有界元依赖原子一样糟糕，在某些情况下甚至更糟，例如，只有两个析取的片段是NP完全的。此外，我们几乎完全分类的计算复杂性的模型检验问题的所有限制的命题和模态算子的无界以及有界MDL。
2012-01-27 cs.CC cs.LO
Incremental Symbolic Bounded Model Checking of Software Using Interval Methods via Contractors
有界模型检验（BMC）对于发现程序属性冲突至关重要。对于不安全的程序，BMC可以快速找到从初始状态到违反状态的执行路径，从而反驳给定的安全属性。然而，BMC技术难以伪造包含循环的程序。BMC需要将程序循环逐步展开到绑定$k$，从而暴露属性冲突，这可能导致探索相当大的状态空间。在这里，我们描述和评估的第一个验证方法的基础上，通过承包商的区间方法，以减少域的变量表示的搜索空间。这种减少是基于建模为代表承包商约束的函数的指定属性。特别是，我们利用区间方法通过承包商增量分析程序循环变量和合同的属性保证举行修剪搜索探索的域，从而减少资源消耗积极。实验结果表明，我们所提出的方法的效率和有效性在一个大的基准集，包括$7044$验证任务，与国家的最先进的BMC工具相比。我们提出的方法可以减少内存使用高达$75$ \%，而验证$1$ \%更多的验证任务。
2022-09-21 cs.LO cs.SE
Bounded Quantifier Instantiation for Checking Inductive Invariants
本文提出有界视界量词实例化方法，限制实例化项深度以保证SMT求解器终止，能有效检查归纳不变量，且界限1时可自动模拟插桩，无需修改代码。
2019-08-20 cs.LO cs.PL
Twin-width I: tractable FO model checking
受Guillemot和Marx [SODA '14]在置换上定义的宽度不变量的启发，我们在图和矩阵上引入了孪生宽度的概念。真次闭类、有界秩宽图、映射图、无$K_t$单位$d$维球图、具有有界大小反链的偏序集以及2维偏序集的真子类都具有有界孪宽。在所有这些类（除了地图图没有几何嵌入），我们展示了如何计算在多项式时间序列的$d$ -收缩，见证双宽度是最多$d$。我们表明，FO模型检验，这是决定如果一个给定的一阶公式$ϕ$评估为真的一个给定的二进制结构$G$域$D$，是FPT在$|ϕ|$上的类有界双宽度，提供了证人。更确切地说，给定$G$的$d$ -收缩序列，我们的算法在时间上运行$f(d,|ϕ|) \cdot |D|$，其中$f$是可计算但非初等的函数。我们还证明了有界双宽度保存FO的解释和转导（允许操作，如平方或补充图）。这统一并显著扩展了关于非单调类上FO模型检验的固定参数易处理性的知识，例如Gajarskeleton等人的有界宽度偏序集上的FPT算法[FOCS '15]。
2021-10-25 cs.DM cs.DS cs.LO
Bounded Model Checking of Multi-threaded Software using SMT solvers
从单核处理器到多核处理器的过渡使得多线程软件成为计算机辅助验证的一个重要课题。在这里，我们描述和评估的ESBMC模型检查器的扩展，以支持验证多线程软件共享的变量和锁使用有界模型检验（BMC）的基础上可满足性模理论（SMT）。我们描述了三种方法来模型检查多线程软件和我们的建模的同步原语的Pthread库。在惰性方法中，我们生成所有可能的交织，并分别对每个交织调用BMC过程，直到我们找到一个bug，或者系统地探索了所有交织。在时间表记录方法中，我们将所有可能的交织编码成一个单一的公式，然后利用SMT求解器的高速。在欠近似加宽方法中，我们通过从SMT求解器生成的不可满足性证明中提取状态变量和交织的数量来减少状态空间。在所有这三种方法中，我们都使用了部分降阶（POR）技术来减少交织的数量。实验表明，我们的方法可以分析更大的问题，并大大减少验证时间相比，国家的最先进的技术，结合经典的POR方法与符号算法和其他实现反例引导抽象细化技术。
2010-03-19 cs.LO cs.SE
Incremental Bounded Model Checking of Artificial Neural Networks in CUDA
Federal University of Amazonas（亚马逊联邦大学）；SIDIA Instituto de Ciência e Tecnologia（SIDIA科学技术研究所）；University of Manchester（曼彻斯特大学）
人工神经网络（ANN）是用于各种应用的强大的计算系统，这是由于其通用性来概括和响应意外的输入/模式。然而，人工神经网络的安全关键系统的实现可能会导致故障，这是很难预测的设计阶段，因为人工神经网络是高度并行的，他们的参数是很难解释。在这里，我们开发并评估了一种基于增量有界模型检验（BMC）的新型符号软件验证框架，以检查多层感知器（MLP）中的对抗性情况和覆盖方法。特别是，我们进一步开发了高效的基于SMT的图形处理单元上下文有界模型（ESBMC-GPU），以确保某些安全属性的可靠性，其中安全关键系统可能会出现故障并做出错误的决策，从而导致不必要的材料损坏甚至危及生命。本文标志着第一个符号验证框架的原因在CUDA实现的人工神经网络。我们的实验结果表明，我们在ESBMC-GPU上实现的方法可以成功地验证人工神经网络的安全属性和覆盖方法，并正确地生成28个MLP对抗案例。
2019-07-30 cs.LG cs.LO cs.NE
Some approximations in Model Checking and Testing
模型检验和测试是两个具有相似目标的领域：验证系统是否满足属性。他们从系统的不同假设开始，并开发了许多具有不同近似概念的技术，当精确的验证可能在计算上太难时。本文介绍了近似的概念及其逻辑和统计背景，并由此引出了几种模型检验和测试技术：有界模型检验、近似模型检验、近似黑盒检验、近似基于模型的测试和近似概率模型检验。所有这些方法都保证了验证的质量和效率。
2013-04-16 cs.LO cs.SE
A New Perspective on FO Model Checking of Dense Graph Classes
本文研究稠密图的一阶（FO）模型检验问题，即那些在稀疏图类中具有FO解释（或者是FO转换）的图。给出了在有界度图中FO可解释的图类的结构特征。这种特征使我们能够有效地计算输入图的FO解释。因此，我们得到了一个FPT算法的后继不变的FO模型检验的任何图形类，这是FO解释（或FO转换）的图类的有界度。我们用来获得这些结果的方法也可能是独立的利益。
2018-05-04 cs.DM cs.LO math.CO
Bounded game-theoretic semantics for modal mu-calculus
我们引入了一个新的博弈论语义（GTS）的模态μ演算。我们所谓的有界GTS取代奇偶游戏与替代评估游戏，只有有限的路径出现，无限的路径是不需要的，即使当考虑的过渡系统是无限的。新的游戏提供了替代方法的各种建设的框架中的μ演算。例如，它们已经成功地用作一种方法的基础，这种方法导致逻辑的自然公式大小游戏。虽然我们的主要重点是介绍新的GTS，我们也考虑一些应用程序来演示其用途。例如，我们考虑一个自然的模型转换过程，减少模型检查游戏，检查一个单一的，固定的公式在构建的模型，我们还使用GTS识别新的替代变种的μ演算与PTime模型检查。
2020-05-21 cs.LO math.LO
Optimizing Epistemic Model Checking using Conditional Independence
条件独立推理已经被证明在贝叶斯网的上下文中有助于优化概率推理，并且相关技术已经被应用于通过消除公式的不相关部分来加速布尔逻辑中的许多逻辑推理任务。本文表明，条件独立推理也可以应用于优化认知模型检验，其中一个验证，一个模型的一些代理不完善的信息满足一个公式表示的知识模态多代理逻辑。开发了一种优化技术，该技术在使用模型检验算法之前进行分析，该分析应用条件独立推理来减小模型的大小。该优化已在认知模型检测器MCK中实现。本文报告的实验结果表明，它可以产生多个数量级的性能改善。
2016-10-13 cs.LO
Synthesizing Update Schedules with Game-Based Extension of Bounded Model Checking
Carl von Ossietzky Universität Oldenburg（奥尔登堡卡尔·冯·奥西茨基大学）
针对安全关键系统无中断安全软件更新的难题，提出将系统与更新交互建模为双人时间博弈、用有界SMT编码合成全局固定更新调度的方法，经自动驾驶轨迹规划器示例验证可保障所有可允许执行下的安全部署。
2026-09-28 cs.GT cs.LO
On the Parameterized Intractability of Monadic Second-Order Logic
Courcelle的一个著名结果是：如果C是一类有界树宽的图，则一元二阶逻辑（MSO_2）的模型检验是C上的固定参数线性时间参数化算法可处理的（fpt），其中参数是树宽加上公式的大小。一个直接的问题是，这是否是最好的，或者结果是否可以扩展到无限树宽的类。在本文中，我们表明，在树的宽度，定理不能进一步推广。更具体地说，我们证明了，如果C是一类图，这是封闭的着色，并满足一定的构造性条件，是这样的树宽度不受\log^{84} n，那么MSO_2-模型检验不是FPT，除非SAT可以解决在次指数时间。如果C的树宽不是多项式有界的，则MSO_2-模型检验不是fpt，除非多项式时间层次中的所有问题都能在次指数时间内求解。
2012-03-23 cs.LO
Sound Statistical Model Checking for Probabilities and Expected Rewards (extended version)
本文综述了统计模型检验工具的可靠性，提出用Dvoretzky-Kiefer-Wolfowitz不等式估计期望奖励，并实现于'modes'工具，实验验证了其有效性。
2025-09-12 cs.LO
Decomposition Theorems and Model-Checking for the Modal $μ$-Calculus
我们证明了一个一般的分解定理的模式$μ$ -演算$L_μ$的精神Feferman和Vaught的定理不相交的工会。特别是，我们表明，如果一个结构（即，转换系统）由两个子结构$M_1$和$M_2$加上从$M_1$到$M_2$的边组成，则在$M$中的节点处的公式真仅取决于在相应子结构中的公式真，其意义在下面进行精确说明。因此，我们证明了$L_μ$的模型检测问题是固定参数易处理的（FPT）类结构的有界凯利宽度或有界DAG宽度。据我们所知，这些是$L_μ$的第一个FPT结果，它不遵循嵌入到一元二阶逻辑中。
2014-05-09 cs.LO math.LO
Tarmo: A Framework for Parallelized Bounded Model Checking
本文研究了共享内存环境和工作站集群环境下的有界模型检验（BMC）并行化方法。我们提出了一个通用的框架，并行BMC命名为Tarmo。我们的框架可以与BMC的任何增量SAT编码一起使用，但对于本文中的结果，我们仅使用当前最先进的完整PLTL编码。使用这种编码允许我们检查安全性和活性属性，这与早期分发BMC时仅限于安全属性的工作相反。尽管我们的重点是BMC后，它已被翻译成SAT，现有的分布式SAT求解器并不适合我们的应用程序。这是因为解决BMC问题不是解决一组独立的SAT实例，而是解决多个相关的SAT实例，增量编码，其中每个实例的可满足性对应于特定长度的反例的存在。我们的框架包括一个通用的共享子句数据库的架构，允许SAT求解线程之间轻松共享子句解决各种这样的实例。我们提出了广泛的实验结果与我们的Tarmo实现的多个变体。我们的共享内存变体比传统的单线程方法具有更好的性能，这是许多用户可以受益于多核和多处理器技术的广泛应用的结果。此外，我们证明了我们的框架可以部署在一个典型的工作站集群，其中几个多核机器通过网络连接。
2009-12-13 cs.DC cs.LO
MPBMC: Multi-Property Bounded Model Checking with GNN-guided Clustering
Indian Statistical Institute（印度统计研究所）；IBM Systems（IBM系统公司）；Texas Instruments（德州仪器）
本文提出基于图神经网络的多属性有界模型检查方法，通过功能聚类提升多属性验证效率。
2026-02-26 cs.AI cs.LG cs.LO
Context-Bounded Model Checking for POWER
基于Qadeer等人在2005年提出的用于检测并发程序（假定运行在经典SC模型下）中bug的上下文有界分析的工作，我们提出了一种针对POWER内存模型下运行的程序的欠近似可达性分析算法.为此，我们首先引入了一个新的上下文绑定概念，它适用于POWER下的计算推理，它概括了Atig等人在2011年为TSO内存模型定义的概念。然后，我们提供了一个多项式大小减少的上下文有界状态的可达性问题下POWER SC下相同的问题：给定一个输入并发程序P，我们的方法产生一个并发程序P'，这样，对于一个固定数量的上下文切换，运行P' SC下产生相同的一组可达状态下运行P POWER。生成的程序P'包含与P相同数量的进程，并且在相同的数据域上操作。通过利用标准的模型检查器CBMC，我们已经实现了一个原型工具，并将其应用于一组基准测试，表明我们的方法的可行性。
2019-09-24 cs.FL cs.LO cs.PL
