Symbolic model checking of tense logics on rational Kripke models
本文引入了有理Kripke模型类，研究了基本时态逻辑Kt的符号模型检验及其在该类模型中的一些扩展。有理Kripke模型基于（通常是无限的）有理图，顶点由某些正则语言中的单词标记，转换由异步双头有限自动机（也称为有理转换器）识别。在理性Kripke模型中，每个原子命题都在一组规则的状态中求值。证明了Kt的每个公式在每个有理Kripke模型中都有一个有效的可计算正则扩张，从而证明了有理Kripke模型中Kt的局部模型检验和全局模型检验是可判定的.这些结果被提升到Kt的一些扩展。我们研究并部分确定了模型检验过程的复杂性。
2008-10-30 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
SMT Queries Decomposition and Caching in Semi-Symbolic Model Checking
在半符号（控制-显式数据-符号）模型检验中，状态空间爆炸问题通过位向量理论上的一阶公式表示状态集来解决。在这种模型检验方法中，大部分验证时间都花在SMT求解器上，用于确定量化查询的可满足性，这些量化查询表示符号状态的相等性。在本文中，我们介绍了一个新的计划分解的符号状态，它可以用来显着提高任何半符号模型检查器的性能。使用分解，与原始情况相比，模型检查器可以向求解器发出更简单和更小的查询。一些SMT调用甚至可以完全避免，因为一些简化公式的满足可以从语法上决定。此外，分解允许用于量化公式的高效缓存方案。为了支持我们的理论贡献，我们展示了我们的模型检查器SymDIVINE的性能增益的一组例子，从软件验证比赛。
2017-11-20 cs.LO cs.PL
Bandwidth and Wavefront Reduction for Static Variable Ordering in Symbolic Model Checking
我们证明了带宽和波前减少算法的适用性静态变量排序。在符号模型检验中，事件局部性在时间和内存使用方面起着重要作用。例如，在Petri网中，事件局部性可以通过依赖矩阵来捕获，其中非零条目指示转换是否修改了位置。事件局部性的质量被表示为称为（加权）事件跨度的度量。矩阵的带宽是一个度量，表示非零元素到对角线的距离。波前是指示矩阵对角线一端上的非零程度的度量。带宽和波前是稀疏矩阵解算器中使用的已充分研究的度量。在这项工作中，我们证明了跨度是有限的两倍的带宽的矩阵。这种观察使得带宽减少算法对于获得良好的可变阶数是有用的。我们解决的一个主要问题是，约简算法只能应用于对称矩阵，而依赖矩阵是不对称的。我们表明，Sloan算法上执行的邻接图的总图给出了最好的变量顺序。实际上，我们证明了我们的工作允许在Boost和ViennaCL中调用标准稀疏矩阵操作，在毫秒内计算非常好的静态变量顺序。未来的工作是有希望的，因为一个全新的频谱更多的现成的算法，包括元启发式的，成为变量排序。
2015-11-27 cs.LO cs.SE
Irene: Equivalence Checking of Hybrid Quantum Programs via Structure-Preserving Symbolic Reduction
Shanghai Jiao Tong University（上海交通大学）
提出Irene框架，通过保结构符号化简在门级、混合路径和及密度核三个层次验证混合量子程序等价性，在1982个程序对中解决79.92%，并发现15个编译器缺陷。
2026-09-30 cs.LO cs.PL cs.SE
The Complexity of Checking Non-Emptiness in Symbolic Tree Automata
该研究将符号树自动机的可满足性问题分解为两类理论的可满足性问题，进而得到该类自动机及其带线性算术约束扩展的判定问题的紧计算复杂度界。
2023-11-09 cs.FL cs.LO
From Bounded Checking to Verification of Equivalence via Symbolic Up-to Techniques
我们提出了一个有界等价性验证技术的高阶程序与局部状态。该技术结合了完全抽象的符号环境互模拟类似的符号游戏语义，新的技术，轻量级的状态不变的注释。这产生了没有假阳性或假阴性的等效性验证技术。该技术是有界完备的，因为所有的不等式都是自动检测到足够大的界限。此外，几个硬等价证明自动或后被注释与状态不变量。我们在一个名为Hobbit的工具原型中实现了该技术，并使用一组广泛的新的和现有的示例对其进行基准测试。霍比特人可以证明许多经典的等价关系，包括所有迈耶和西伯的例子。
2021-10-22 cs.LO cs.PL
SMT-based Symbolic Model-Checking for Operator Precedence Languages
针对现有POTL显式状态模型检测方法可扩展性差的问题，本文提出首个基于SMT的符号化方法，将POTL公式与程序模型编码为SMT公式，通过求解器以有界模型检测方式搜索反例轨迹，实验验证了方案有效性。
2024-05-18 cs.LO
Symbolic Model Checking in External Memory
本研究为外部存储器BDD包Adiar扩展单调变量替换支持以实现关系积运算，优化后小BDD模型检测速度最高提47%，其I/O高效性使其受内存影响小，大实例下远快于同类工具CAL。
2025-05-16 cs.DS cs.LO
Exploiting Asymmetry in Logic Puzzles: Using ZDDs for Symbolic Model Checking Dynamic Epistemic Logic
University of Groningen（格罗宁根大学）；University of Amsterdam（阿姆斯特丹大学）
本文提出用ZDDs替代BDDs对动态认知逻辑中的Kripke模型进行符号编码，并在三个经典多智能体谜题上验证了该方法可显著降低模型检测的内存使用。
2023-07-11 cs.AI cs.LO
Combining Explicit and Symbolic Approaches for Better On-the-Fly LTL Model Checking
我们提出了两种新的混合技术，取代同步产品中使用的自动机理论方法的LTL模型检验。建议的产品是明确的图形的聚集（符号集的状态），可以解释为Büchi自动机。这些混合方法一方面允许使用经典的空检查算法并在运行中构建图，另一方面，由于聚集体的符号表示，具有状态空间的紧凑编码。符号观测产品假设全局断续属性（例如，LTL \ X）来聚合状态。自循环聚合产品}不要求属性是全局断续的（即，它可以处理完整的LTL），但在可能的情况下动态地检测和利用一种形式的口吃。我们的实验表明，这两个变种，而彼此无法比拟的，可以优于其他现有的方法。
2011-06-28 cs.FL cs.LO
Dynamic Reductions for Model Checking Concurrent Software
并行程序的符号模型检验是解决交织爆炸问题的有效方法。我们提出了一个动态减少技术，以避免不必要的交织。通过扩展Lipton的原始工作与双相似性的概念，我们容纳动态事务，从而减少依赖于静态分析，这是一个严重的瓶颈，在其他减少技术的准确性。结合符号模型检验和动态约简技术已被证明是具有挑战性的，在过去。尽管如此，我们的通用归约定理使我们能够推导出一种有效的符号编码，我们为IC3和BMC实现了这种编码。实验证明了几个案例研究和一个大的SVCOMP基准动态减少的权力。
2016-11-28 cs.FL cs.LO
Satisfiability Checking and Symbolic Computation
符号计算和可满足性检验被视为独立的研究领域，但它们在算术理论决策过程的开发、实现和应用方面有着共同的兴趣。尽管有这些共同点，但这两个社区目前只有微弱的联系。我们引入了一个新的项目SC-广场，以在该地区建立一个联合社区，并得到新接受的同名欧盟（H2020-FETOPEN-CSA）项目的支持。我们的目标是通过创建共同的平台，启动互动和交流，确定共同的挑战，并制定共同的路线图，加强这些社区之间的联系。这张摘要和随附的海报描述了该项目的动机和目标，并报告了第一批活动。
2016-07-23 cs.LO cs.SC
Satisfiability Checking meets Symbolic Computation (Project Paper)
符号计算和可满足性检验是两个研究领域，两者在算术理论决策过程的发展、实现和应用方面有着各自的科学重点，但也有着共同的兴趣。尽管有共同点，但这两个社区的联系相当薄弱。我们新接受的SC-square项目（H2020-FETOPEN-CSA）的目的是通过创建共同平台，启动互动和交流，确定共同挑战，以及开发从理论到工具和（工业）应用的共同路线图来加强这些社区之间的联系。在本文中，我们报告的目标和该项目的第一次活动，并正式确定了一些相关的挑战，为统一的SC广场社区。
2016-07-27 cs.LO cs.SC
Software Model Checking with Explicit Scheduler and Symbolic Threads
在许多实际的应用领域中，软件被组织成一组线程，其激活是排他性的，并由一个合作的调度策略控制：线程执行，没有任何中断，直到它们终止或明确地将控制权交给调度程序。这种软件的形式化验证提出了重大挑战。一方面，每个线程可能有无限的状态空间，并且可能需要抽象。另一方面，调度策略通常对于正确性很重要，并且基于抽象调度器的方法可能导致精度损失和误报。不幸的是，将问题转化为纯粹的顺序软件模型检验问题对于现有技术来说是非常低效的。我们提出了一种利用这些程序的内在结构的软件模型检验技术。每个线程都被转换成一个单独的顺序程序，并通过惰性抽象进行象征性的探索，而整体验证则由调度程序的直接执行来协调。该方法是通过过滤的探索调度器与偏序约简的集成优化。该技术，称为ESST（显式线程，符号线程）已实施和实验评估的一组重要的基准。结果表明，ESST技术是更有效的方式比软件模型检验应用于序列化程序，和偏序约简可以导致进一步的性能改善。
2012-07-31 cs.LO cs.PL
Comparing State-Representations for DEL Model Checking
ILLC, University of Amsterdam（阿姆斯特丹大学计算逻辑与系统研究所）；Chennai Mathematical Institute（金奈数学研究所）
本文比较了 DEL 模型检查中符号结构和心理程序的表示方法，证明了其理论复杂性，并提供了两种转换的直接方法。
2025-11-27 cs.LO cs.MA
Debugging Smart Contract's Business Logic Using Symbolic Model-Checking
智能合约是在区块链内部运行的一种特殊类型的程序。它们是不可变和透明的，提供了实现容错和抗审查服务的方法。不幸的是，它的不变性导致了一个严重的挑战，即在区块链中发布之前，确保业务逻辑和实现是正确的。几起重大事故确实表明，这项技术的用户需要特殊的工具来验证智能合约的正确性。现有的自动检查器只能检测已知的实现错误，而将业务逻辑正确性问题远远抛在一边。在这项工作中，我们提出了一个象征性的模型检验技术，以及一个正式的规格说明方法的一个子集的Solidity程序设计语言，能够表达状态属性和跟踪属性，后者构成了一个弱的类比的时间属性。我们在MiniDAO智能合约上评估了所提出的技术，MiniDAO是臭名昭著的TheDAO的年轻兄弟。我们的概念验证能够在几秒钟内检测到这个智能合约的业务逻辑中的一个重要错误。
2018-12-03 cs.CR cs.LO cs.PL
Symbolic and Structural Model-Checking
本文提出结合SMT过近似、无记忆采样欠近似和结构化简规则，使模型检验复杂度与网结构而非状态空间成正比，并在2020年模型检验竞赛中赢得可达性查询和死锁检测。
2021-12-18 cs.DC cs.FL cs.LO
Towards Symbolic Factual Change in DEL
我们扩展了符号模型检验的动态认知逻辑（DEL）的事实变化。我们的Transformers提供了一个紧凑的表示动作模型的前置和后置条件，为S5和一般情况下。该方法可以实现使用二进制决策图，我们希望它能提高模型检验性能。作为一个例子，我们给萨利-安妮错误信念任务的象征性表示。
2019-12-23 cs.LO cs.SC
A Backward-traversal-based Approach for Symbolic Model Checking of Uniform Strategies for Constrained Reachability
自从交替时间时序逻辑（ATL）被引入以来，许多逻辑被提出来推理系统中智能体的不同策略能力。特别是，一些逻辑已经被设计成这样的代理商的统一的无记忆策略的原因。这些策略是智能体可以通过只看他们从当前状态观察到的东西来有效地发挥作用的策略。ATL_ir可以被看作是推理这种统一策略的核心逻辑。然而，它的模型检查问题是困难的（它需要对NP预言机的多项式次数的调用），并且解决它的实用算法直到最近才出现。本文提出了一种模型检验统一无记忆策略技术。现有技术通过系统的前向遍历从感兴趣的状态（诸如初始状态）构建策略。另一方面，所提出的方法通过向后遍历从目标状态构建获胜策略，确保只探索统一的策略。然而，从头开始构建策略将其适用性仅限于受限的可达性目标。本文详细介绍了这种方法，并将其与现有的方法实现到一个基于BDD的框架实验比较。这些实验表明，该技术是有竞争力的情况下，它可以处理。
2017-09-07 cs.LO
On the size of data structures used in symbolic model checking
Dipartimento di Informatica e Sistemistica（信息与系统学系）；Sapienza Università di Roma（罗马第一大学）
时态逻辑模型检验是一种验证方法，它通过对系统模型的描述，来验证系统中的某些属性（用时态逻辑公式表示）是否成立。它有许多工业应用。为了提高性能，一些工具允许预处理的模型，验证在线的一组属性重用相同的编译模型，我们证明了模型检验问题的复杂性，没有任何预处理或预处理的模型或多项式数据结构中的公式，是相同的。因此，预处理并不总是以指数方式提高性能。符号模型检验算法通过操作状态集来工作，这些状态集通常由BDD表示。已经观察到，BDD的大小可以随着模型和公式的大小的增加而指数地增长。作为一个副作用，我们正式证明，这些BDD的大小的超多项式增加是不可避免的，在最坏的情况下。虽然这种指数增长已被经验观察到，但据我们所知，迄今为止还没有得到一般性的证明。这个结果不仅适用于所有类型的BDD，而不管变量的顺序如何，而且适用于更强大的数据结构，如BED、RBC、MTBDD和ADD。
2010-12-14 cs.AI cs.CC cs.DS
Formal Verification of Safety Properties Using Interpolation and k-induction
本技术报告介绍了使用SAT/SMT求解器的两种符号模型检验算法的实现，即基于插值的模型检验和基于k-归纳的模型检验。并对这两种模型检验算法进行了比较分析。
2022-07-04 cs.LO
Symbolic bisimulation for quantum processes
利用文献中提出的互模拟概念，为了检验两个量子过程是否互相似，我们必须用任意量子态实例化它们的自由量子变量，并验证结果组态的互相似性。这使得从算法的角度来看，检查双相似性是不可行的，因为量子态构成了一个连续统。在本文中，我们直接在量子操作层次上引入了一种量子过程的符号操作语义，它允许我们描述量子过程之间的互模拟，而无需求助于量子态。我们表明，这里定义的符号互模拟是等价的开放互模拟量子过程在以前的工作中，当考虑强互模拟。提出了一种符号基双相似性检验算法。基于Hennessy-Milner逻辑对量子过程的扩展，我们给出了量子双相似性的模态逻辑刻画。
2012-02-21 cs.LO
PrIC3: Property Directed Reachability for MDPs
IC 3是符号模型检验的一次飞跃。本文提出了PrIC 3（发音为pricy-three），一个保守的扩展IC 3的符号模型检验的MDP。我们的主要重点是发展PrIC 3的理论基础。此外，我们还介绍了PrIC 3的第一个实现，包括IC 3的关键成分，如泛化，重推和传播。
2020-05-18 cs.LO
Experiments in Model-Checking Optimistic Replication Algorithms
本文描述了一系列模型检验实验来验证用于支持协同编辑的基于操作转换（OT）方法的乐观复制算法。我们正式定义，使用工具UPPAAL，行为和主要的一致性要求（即收敛性）的协同编辑系统，以及这些系统应该操作的环境的抽象行为。由于数据复制和用户交互的不可预测性，这样的系统有无限多个状态。因此，我们展示了如何利用UPPAAL规约语言的一些功能来减弱严重的状态爆炸问题。提出了两种模型。第一种称为具体模型，它非常接近系统实现，但会遇到严重的状态爆炸。第二种模型称为符号模型，旨在通过延迟编辑操作的有效选择和执行，直到所有站点的符号执行痕迹构建完成，来克服具体模型的局限性。实验结果表明，符号模型允许在空间和时间上的显着增益。使用的符号模型，我们已经能够表明，如果网站的数量超过2，那么收敛性不满足所有OT算法在这里考虑。每个算法都有一个反例。
2008-04-21 cs.LO cs.SC
Experience with Heuristics, Benchmarks & Standards for Cylindrical Algebraic Decomposition
在激发SC广场项目的论文中，[E。Abraham，在符号计算和可满足性检查之间建立桥梁，Proc. ISSAC '15，pp. 1-6，ACM，2015]作者将复杂的逻辑学的使用确定为可满足性检查社区擅长的技术，并且符号计算社区可能从中学习和繁荣。为了开始这个学习过程，我们总结了计算机代数算法柱形代数分解的启发式开发经验。我们还提出并讨论了标准和基准，作为符号计算可以从可满足性检查专业知识中蓬勃发展的另一个领域，注意到这些已被确定为CSA项目中新SC Square社区的初始行动，如[E.~ Abraham等人，SC $^2$：可满足性检查符合符号计算（项目论文）}，智能计算机数学（LNCS 9761），pp. 28- 43，Springer，2015]。
2016-09-29 cs.LO cs.SC
Weakly acyclic diagrams: A data structure for infinite-state symbolic verification
针对OBDDs无法处理无限状态系统的局限，提出弱无环图（WADs）这一OBDDs泛化结构，保留其算法优势并支持无限语言表示，可用于多种无限状态系统的符号模型检测。
2025-02-17 cs.DS cs.LO
Static Analysis of Communicating Processes using Symbolic Transducers
我们提出了一个通用模型，允许静态分析的基础上抽象的解释系统的通信过程。我们的技术受到常规模型检验的启发，将程序状态集表示为格自动机，将程序语义表示为符号转换器。该模型可以表示进程和通信的动态创建/销毁。使用抽象的解释框架，我们能够提供一个健全的过度近似的系统的可达集，从而使我们能够证明安全属性。我们在一个原型中实现了这种方法，该原型针对C程序的MPI库。
2016-11-27 cs.FL cs.LO cs.SE
FO model checking of geometric graphs
在过去的二十年里，一阶（FO）模型检验算法的研究主要集中在稀疏关系结构上--最终由Grohe、Kreutzer和Siebertz提出的FPT算法，用于对无处密集的图类进行FO模型检验。与此相反，除了局部有界的顶点宽度的情况下，只有很少的是目前所知的密集类的图或其他结构的FO模型检验。我们研究的FO模型检验问题的稠密图类定义的几何手段（相交和可见性图）。我们得到新的非平凡FPT结果，例如，对于圆弧、圆、盒、盘和双可见性图的受限子类。这些结果使用FPT算法Gajarskeleton等人。有界宽度偏序集的FO模型检验。我们还通过相关的硬度降低来补充易处理性结果。
2018-03-26 cs.LO
On the Verification of a WiMax Design Using Symbolic Simulation
在自顶向下的多层次设计方法中，在更高抽象层次上的设计描述被逐步细化到最终实现。基于仿真的技术传统上被用于验证这种模型改进不会改变设计功能。不幸的是，利用计算机模拟，不可能在合理的时间内完全检查设计变换是否正确，因为这样做所需的测试模式的数量随着系统状态变量的数量呈指数级增加。在本文中，我们提出了一种方法，用于验证在设计过程中产生的模型在更高的抽象层次的设计规范的一致性。我们使用递归方程的序列建模系统的行为。然后，我们使用符号模拟与等价性检查和属性检查技术的设计验证。使用我们提出的方法，我们已经验证了三个WiMax系统模型在不同层次的设计抽象的等效性，以及这些模型上的各种系统属性的正确性。我们的符号建模和验证实验表明，所提出的验证方法提供了其数值对应的性能优势。
2013-07-31 cs.LO
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
Formal Security Analysis of Neural Networks using Symbolic Intervals
Columbia University（哥伦比亚大学）
由于深度神经网络（DNN）在现实世界的安全关键领域（包括自动驾驶汽车和防撞系统）中的部署越来越多，因此正式检查DNN的安全属性（特别是在不同的攻击者能力下）变得至关重要。大多数现有的DNN安全测试技术都试图找到对抗性示例，而没有提供任何关于此类对抗性示例不存在的正式安全保证。最近，有几个项目使用不同类型的可满足性模理论（SMT）求解器来正式检查DNN的安全属性。然而，所有这些方法都受到求解器引起的高开销的限制。在本文中，我们提出了一个新的方向，正式检查DNN的安全属性，而不使用SMT求解器。相反，我们利用区间算术来计算DNN输出的严格边界。我们的方法，不像现有的基于求解器的方法，很容易并行化。我们进一步提出了符号区间分析以及其他几个优化，以尽量减少高估的输出界。我们设计，实现和评估我们的方法作为ReluVal的一部分，正式检查基于Relu的DNN的安全属性的系统。我们广泛的实证结果表明，ReluVal比Reluplex（一种最先进的基于求解器的系统）平均高出200倍。在没有GPU的8核机器上，ReluVal能够在4小时内验证Reluplex认为由于运行超过5天后超时而无法确定的安全属性。我们的实验表明，符号区间分析是一个有前途的新方向，严格分析DNN的不同安全属性。
2018-07-01 cs.AI cs.LO
OCTAL: Graph Representation Learning for LTL Model Checking
Purdue University（普渡大学）
针对传统符号模型检测的状态空间爆炸问题，提出基于图表示学习的OCTAL框架，将LTL模型检测转化为二分类任务，实现了显著的准确率与最高11倍的整体加速。
2023-08-19 cs.AI cs.LO cs.SE
Verifying Reachability Properties in Markov Chains via Incremental Induction
在概率验证和非概率验证之间存在可扩展性差距。概率模型检验工具基于显式引擎或（多端）二元决策图。这些结构在非概率验证领域得到了更可扩展的技术（如IC3）的补充。我们提出了一个符号概率模型检验算法的基础上IC3类增量建设的归纳条款划分的状态空间，交错与增量建设的线性不等式系统。本文比较了我们的实现标准的定量验证的替代方案：我们的实验表明，我们的算法是一个步骤，以更可扩展的符号验证有限状态马尔可夫链中的罕见事件。
2019-09-19 cs.LO
Symbolic Optimal Reachability in Weighted Timed Automata
加权时间自动机在2000年初被定义用于建模实时系统中的资源消耗或分配问题。在加权时间自动机中，最优可达性是可判定的，并提出了一种符号前向算法来解决这一问题。该算法使用所谓的定价区域，即具有成本函数的标准区域的扩展。为了确保终止，该算法要求时钟有界。对于未定价的时间自动机，已经做了很多工作来开发适合于时间自动机的前向探索的合理抽象，确保在不限制时钟的情况下终止模型检查算法。在本文中，我们利用最近的发展抽象的时间自动机，并提出了一个算法，允许符号分析的所有加权时间自动机，而不需要有界的时钟。
2016-02-01 cs.LO
Modeling and Verification of Agent based Adaptive Traffic Signal using Symbolic Model Verifier
本文讨论了多Agent系统（MAS）场景的建模与验证问题。我们已经考虑了基于代理的自适应交通信号系统。该系统监测两个路段交叉口的交通畅通。在描述了如何有效地使用自适应交通信号灯系统，并显示其优势，交通信号与预定的周期，我们已经展示了如何将这种情况下，我们可以转换为有限状态机（FSM）。一旦系统被转换成FSM，我们已经验证了规范中指定的计算树逻辑（CTL）使用NuSMV作为模型检验工具。从NuSMV获得的仿真结果表明，我们是否满足系统的规格或不。它还向我们展示了系统规范不成立的状态。使用它我们可以追溯到我们的系统，找到源，导致规范违反。最后，我们再次验证了修改后的系统与NuSMV的规格。
2012-08-16 cs.LO cs.SE
Model-Checking Process Equivalences
过程等价是一种形式化的方法，它将程序和系统联系起来，这些程序和系统在非正式的情况下以相同的方式运行。由于没有唯一的概念，这意味着两个动态系统显示相同的行为有大量的形式过程等价，从互模拟跟踪等价，分类在线性时间分支时间谱。我们提出了一个逻辑框架的基础上表达模态不动点逻辑，它是能够定义许多过程等价关系：对于每个这样的等价有一个固定的公式，这是满足一对过程，当且仅当他们是等价的，就这个关系。我们解释了如何做模型检验，甚至象征性地，这个逻辑的一个重要片段，捕捉许多过程的等价。这允许将模型检验技术用于过程等价性检验。我们展示了如何部分评估可以用来获得决策程序的通用模型检验计划的过程等价。
2012-10-09 cs.LO
First-Order Model Checking on Structurally Sparse Graph Classes
一类图是结构无处稠密的，如果它可以通过一阶转换从无处稠密类构造出来。在结构上无处稠密类极大地推广了无处稠密类，并构成了单子稳定类的重要例子。我们表明，一阶模型检验问题是固定参数听话的每一个结构无处密集类图。我们的结果建立在最近开发的一元稳定的图类的博弈论表征。作为独立兴趣的第二个关键成分，我们提供了一个多项式时间算法近似弱邻域覆盖（一般图）。我们将这两个工具结合成一个递归的基于局部性的模型检验算法。该算法对所有允许翻转闭合稀疏邻域覆盖的单子稳定图类都是有效的，其中翻转闭合是一个温和的附加假设。因此，建立有效的一阶模型检验单子稳定类减少到证明存在的翻转封闭的稀疏弱邻域覆盖这些类-一个纯粹的组合问题。我们完成了图片证明所需的覆盖结构无处密集类的存在：我们表明，每一个结构无处密集类可以通过收缩局部顶点集稀疏化，使我们能够解除覆盖稀疏类的存在。
2023-02-07 cs.DM cs.DS cs.LO
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
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
Symbolic Verification and Strategy Synthesis for Turn-based Stochastic Games
随机博弈是一种方便的形式主义建模系统，包括理性的代理人在不确定的环境中竞争或合作。这类模型的概率模型检验技术使我们能够正式指定定量规格的集体或个人的行为，然后自动合成的策略，这些规格下的代理保证得到满足。虽然在算法和工具支持方面取得了良好的进展，但效率和可扩展性仍然是一个挑战。在本文中，我们研究了基于多终端二叉决策图的符号实现。我们描述了如何建立和验证回合制随机游戏对零和或纳什均衡为基础的时间逻辑规范。我们整理了这类游戏的一组基准，并评估我们的方法的性能，表明它在许多情况下是优越的，并且以象征性的方式合成的策略可以更加紧凑。
2022-11-11 cs.LO
Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic
我们介绍堆自动机，一个形式主义的符号堆碎片的分离逻辑与用户定义的归纳谓词的鲁棒性自动推理。可满足性、可达性和非循环性等鲁棒性属性对于基于分离逻辑的自动程序分析和验证中的各种推理任务都很重要。以前，这样的性质已经出现在分离逻辑文献的许多地方，但没有被系统地研究。在本文中，我们开发了一个基于堆自动机的算法框架，使我们能够以统一的方式获得广泛的鲁棒性的渐近最优决策程序。我们实现了我们的框架的原型，并取得了可喜的成果，所有上述的鲁棒性。此外，我们证明了堆自动机的适用性超出了鲁棒性。我们应用我们的算法框架的模型检验和蕴涵问题的符号堆分离逻辑。
2016-10-22 cs.LO
Symbolic Analysis and Parameter Synthesis for Time Petri Nets Using Maude and SMT Solving
带抑制弧的参数时间Petri网（PITPN）允许参数在触发范围内，从而支持时间系统的灵活性。本文提出并证明了PITPN的一种具体的和符号化的重写逻辑语义。我们将展示如何使用Maude结合SMT解决方案，为PITPN提供完善的正式分析。我们开发了一个新的通用折叠符号可达性的方法，终止时的参数状态类图的PITPN是有限的。我们解释了几乎所有的形式分析和参数合成支持的国家的最先进的PITPN工具Roméo可以在Maude与SMT。此外，我们还支持从参数化初始标记进行分析和参数合成，以及使用用户定义的执行策略进行完整的LTL模型检验和分析。在三个基准上的实验表明，我们的方法在许多情况下优于Roméo。
2023-03-15 cs.LO
Verifying Probabilistic Timed Automata Against Omega-Regular Dense-Time Properties
概率时间自动机（Probably Timed Automata，PTAs）是一种扩展了离散概率分布的时间自动机（Timed Automata，TA），它作为一种数学模型，广泛应用于随机和时间行为。在这项工作中，我们考虑的问题，模型检查的线性\emph{dense-time}性质在{PTA}。特别是，我们研究了线性密集时间属性，可以编码的TA与无限的验收criterion.First，我们表明，模型检查PTA对确定性TA规格的问题可以通过产品建设解决。基于乘积结构，证明了确定性TA规格问题的计算复杂性是EXPTIME-完全的。然后我们证明了当放宽到一般的（非确定性的）TA时，模型检测问题变得不可判定，我们的结果大大扩展了TA的稠密时间特性和非确定性。
2018-06-13 cs.FL cs.LO
ATL*AS: An Automata-Theoretic Approach and Tool for the Verification of Strategic Abilities in Multi-Agent Systems
Imperial College London（帝国理工学院）
本文提出面向无限迹与有限迹语义的 ATL* 符号化模型检测算法，并在 ATL*AS 工具中实现，实验证明其在可扩展性和效率上优于现有方法。
2025-10-21 cs.LO cs.MA
Model Checking Probabilistic Real-Time Properties for Service-Oriented Systems with Service Level Agreements
服务质量属性的保证是面向服务的软件工程的一个重要方面。所谓的服务级别协议（SLA）的表示法，例如Web服务级别协议（WSLA）语言，提供了正式的语法来指定服务提供商和客户之间的（具有法律约束力的）合同方面的此类保证。另一方面，用于验证概率实时的【形】行为的形式化方法已经达到了一定的表达能力和效率水平，可以将其应用于现实世界的场景中。本文建议采用最近引入的区间概率时间自动机（IPTA）模型来对面向服务系统的QoS属性进行形式化验证。具体来说，我们表明，IPTA与概率时间自动机（PTA）相比，能够直接捕获SLA中指定的保证。IPTA分析中的一个特殊挑战是，它们的朴素语义通常会产生无限的状态集和无限分支的转换。然而，使用符号表示，IPTA可以进行分析，而有效。我们已经开发了第一个实现的IPTA模型检查器扩展的PRISM工具，并表明，模型检验IPTA是只稍微贵于模型检验可比PTA。
2011-11-14 cs.LO cs.PF cs.SE
Checking Continuous Stochastic Logic against Quantum Continuous-Time Markov Chains
East China Normal University（华东师范大学）；Shanghai Qi Zhi Institute（上海人工智能实验室）；Leiden University（莱顿大学）；Chinese Academy of Sciences（中国科学院）；Institute of Software, Chinese Academy of Sciences（中国科学院软件研究所）；Shanghai University of Finance and Economics（上海财经大学）；Stony Brook University（石溪大学）
本文针对量子连续时间马尔可夫链，提出结合代数与数值方法的连续随机逻辑模型检验方案，确立了CSL的可判定性并保证计算效率，还给出示例演示方法应用。
2025-11-10 cs.LO
Gradual C0: Symbolic Execution for Gradual Verification
本文提出首个实用的递归堆数据结构渐进式验证器 Gradual C0，以符号执行为核心并减少动态检查插入，实证显示其平均运行时开销较完全动态方法降低11%至34%。
2024-01-19 cs.LO
Leveraging the Power of Graph Algorithms: Efficient Algorithms for Computer-Aided Verification
本论文的目标是利用快速图算法和现代算法技术解决图、MDP和博弈图上的模型检验和综合问题。结果包括符号算法，一个众所周知的算法在模型检验，贸易有限的访问输入模型的有效表示。特别是，我们提出了以下结果：算法的游戏图的平均回报Büchi目标和平均回报coBüchi目标相匹配的最佳运行时间的平均回报目标的界限之一。图和MDP中Streett目标的近线性时间随机算法。图中有界Büchi目标的次三次时间算法和对策图的三次时间算法。博弈图和MDP中可达性目标查询的条件下界。图和MDP中顺序可达性目标的线性和近线性时间算法。博弈图中奇偶目标的第一个拟多项式时间符号算法。我们打破了一个长期的运行时间界MEC分解从90年代提供了一个次二次时间符号算法。
2022-02-05 cs.DS cs.LO
On-The-Fly Symbolic Algorithm for Timed ATL with Abstractions
本文在 ADG 框架中提出 TATL 的即时符号验证算法，并通过推广包含检查与新型抽象显著加速，性能优于朴素方法及 Uppaal Tiga。
2025-06-09 cs.LO
Symbolic Algorithms for Language Equivalence and Kleene Algebra with Tests
我们首先提出了一个大字母表上的有限自动机的语言等价性检查算法。我们使用符号自动机，其中的过渡函数是competently表示使用（多端）二进制决策图（BDD）。其关键思想在于通过符号化地探索可达对来计算互模拟，从而避免冗余。这个想法可以结合现有的优化，我们特别显示了一个很好的集成与不相交集森林数据结构从Hopcroft和卡普的标准算法。然后，我们考虑Kleene代数与测试（KAT），代数理论，可用于验证从编译器优化到网络编程分析的各个领域。这个理论是可判定的减少到语言等价的自动机上的保护字符串，一种特殊的自动机，有指数大的字母。我们提出了几种方法，允许构造符号自动机的KAT表达式，根据Brzozowski的衍生物或标准的自动机结构。总而言之，这导致了用于确定KAT表达式的等价性的有效算法。
2014-07-09 cs.FL cs.LO
SMT-based Model Checking for Recursive Programs
提出了一种基于SMT的递归程序安全性验证的符号模型检验算法。该算法是模块化的，并单独分析程序。与其他基于SMT的方法不同，它既保持了程序摘要的“过度近似”，也保持了程序摘要的“欠近似”。欠近似用于分析过程调用，而无需内联。过近似用于阻止不可行的反例和检测收敛到一个证明。我们表明，程序和属性的可判定理论，该算法是保证找到一个反例，如果存在的。然而，效率依赖于用于量词消去（QE）的预言。对于布尔程序，该算法是一个多项式决策过程，匹配最佳BDD算法的最坏情况的界限。对于线性算术（整数和有理数），我们通过“懒惰地”应用QE给出了算法的有效实例。我们使用现有的插值技术来过度近似QE，并引入“基于模型的投影”来欠近似QE。在SV-COMP基准测试上的实验结果表明，该算法在最新水平上有了显著的改进。
2014-05-25 cs.LO
Dense-Timed Petri Nets: Checking Zenoness, Token liveness and Boundedness
我们考虑密集时间Petri网（TPN），Petri网的扩展，其中每个令牌配备有实值时钟，并且语义是懒惰的（即，启用的转换不需要触发;时间可以流逝并禁用转换）。我们考虑了主题方案网络的下列核查问题。(i)Zenoness：是否存在来自给定标记的Zeno计算，即，只需要有限时间的无限计算。我们展示了TPN的zenoness的可判定性，从而解决了[Escrig et al.]的一个开放问题。此外，相关的问题，如果存在任意快速计算从一个给定的标记也是可判定的。另一方面，普遍的zenoness，即，如果所有来自给定标记的无限计算都是zeno，则问题是不可判定的。(ii)Token liveness：标记中的token是否存活，即，是否存在来自标记的最终消耗令牌的计算。我们通过将问题简化为可覆盖性问题来显示问题的可判定性，这对于TPN是可判定的。(iii)有界性：可达标记的大小是否有界。我们考虑两个版本的问题，即语义有界性，只有活令牌被考虑在标记，和语法有界性，也死令牌被认为是。我们展示了语义有界性的不可判定性，同时我们证明了句法有界性是可判定的，通过扩展的Karp-Miller算法。
2007-01-23 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
