Model Checking Event-B by Encoding into Alloy
随着系统变得越来越复杂，验证成为主流。Event-B和Alloy是基于完全不同的方法论的两种正式规约语言。虽然Event-B使用定理证明器来证明不变量适用于给定的规范，但Alloy使用基于SAT的模型查找器。在某些情况下，事件B不变量可能无法自动证明，因此需要交互式证明这一通常很困难的步骤。这个问题的一个解决方案是用模型检验来验证不变量。本文研究了将Event-B机器和上下文编码到Alloy中，以便使用Alloy的基于SAT的引擎执行时态模型检验。
2008-05-30 cs.LO
Model checking and model synthesisfrom partial models: a logic-based perspective
我考虑以下一般情况：一个抽象的模型M的一些“真正的”系统只是部分介绍，或部分已知的，我们必须确保实际的系统满足给定的规范，形式化的一些逻辑语言。这种情况至少有两个本质上不同的解释，导致两个本质上不同的形式逻辑和算法问题：“部分模型的模型合成”，其中M到完整模型的一些“可接受”扩展必须满足规范，和“部分模型的模型检验”，其中M到完整模型的所有“可接受”扩展必须满足规范。这些问题自然地扩展了经典的可满足性、有效性和模型检验的逻辑决策问题。在这里，我简要地讨论这两个问题的背景下，经典，模态和时间逻辑。我做了一些观察，状态一些开放的问题，并概述了一个一般的表格式的程序，解决了几个著名的模态和时序逻辑，包括有限的部分模型的无约束模型合成的问题。K、LTL、CTL、ATL。
2020-12-22 cs.LO
POLIMON: Checking Temporal Properties over Out-of-order Streams at Runtime
本文提出运行时监控工具POLIMON，通过MTL及其冻结量词扩展规约检查系统行为，支持接收并立即处理乱序消息以迅速输出违规判定，适用于验证具有不可靠通道的分布式系统。
2024-04-24 cs.LO
Model Checking of Continuous-Time Markov Chains Against Timed Automata Specifications
我们研究了验证有限连续时间马尔可夫链（CTMC）C对线性实时规范作为一个确定性的时间自动机（DTA）A有限或穆勒接受条件。我们要解决的中心问题是：C的路径集合被A接受的概率是多少，即，C满足A的可能性结果表明，在有限的验收标准，这等于在有限的分段确定性马尔可夫过程（PDP）的可达概率，而Muller验收标准，它符合终端强连通组件在这样的PDP的可达概率。定性验证显示相当于PDP的图形分析。在我们的PDP的可达性概率，然后其特征在于作为第二类Volterra积分方程系统的最小解，并示出近似的偏微分方程系统的解决方案。对于单时钟DTA，该积分方程系统可以被变换成线性方程系统，其中系数是常微分方程的解。由于系数实际上是CTMC中的瞬态概率，因此该结果意味着CTMC分析的标准算法足以验证单时钟DTA规范。
2011-03-27 cs.LO
Hennessy-Milner Logic with Greatest Fixed Points as a Complete Behavioural Specification Theory
有两种根本不同的方法来指定和验证系统的属性。逻辑方法利用规范给出的时间或模态逻辑的公式，并依赖于有效的模型检验算法;行为方法利用各种等价或细化检查方法，提供的规格是在相同的形式主义实现。在本文中，我们提供的最大不动点的Hennessy-Milner逻辑的逻辑形式主义和析取模态转换系统的行为形式主义之间的翻译。我们还介绍了一个新的操作商的上述等价的形式主义，这是伴随的结构组成，并允许合成缺失的规范从部分实现。这是一个实质性的推广商确定性模态过渡系统中定义的早期文件。
2013-06-04 cs.LO
Technical Report: Exploring Automatic Model-Checking of the Ethereum specification
本研究针对以太坊3SF共识协议的可问责安全性，基于其Python规范用TLA+形式化并结合多层手动抽象，通过Apalache等工具实现小规模实例的穷举验证，未发现安全违规，证明了手动抽象对模型检测效率的提升作用。
2025-01-16 cs.DC cs.LO
Probabilistic Model Checking and Autonomy
在不确定或对抗性环境中运行的自治系统的设计和控制可以通过正式的建模和分析来促进。概率模型检验是一种自动验证系统模型是否满足时序逻辑规范的技术，同时也是一种综合最优控制策略的技术。这种方法最近已扩展到多智能体系统，表现出竞争或合作行为建模通过随机游戏和合成的均衡策略。在本文中，我们提供了一个概述的概率模型检验，专注于模型支持的PRISM和PRISM游戏模型检查器。这包括完全可观察和部分可观察的马尔可夫决策过程，以及回合制和并发随机游戏，以及相关的概率时间逻辑。我们证明了该框架的适用性，通过说明性的例子自治系统。最后，我们强调了研究的挑战，并建议在这一领域的未来工作方向。
2021-11-20 cs.LO
Checking the HAL Interface Specification Continuously, Right from the Start
University of Freiburg（弗赖堡大学）；Hahn-Schickard Institute（汉-希克哈德研究所）；Offenburg University（奥芬堡大学）
本文提出了一种持续检查HAL接口规范的方法，从开发一开始就进行检查，通过多次迭代开发嵌入式应用程序，确保每个步骤的检查成功。
2025-12-18 cs.LO cs.SE
Linear-Time Model Checking Branching Processes
（多类型）分支过程是生成随机无限树的自然和充分研究的模型。分支过程具有非确定性和概率性分支，推广了转移系统和马尔可夫链（但不是一般的马尔可夫决策过程）。我们研究了模型检验分支过程对线性时间ω-正则规范的复杂性：它是几乎肯定的情况下，由分支过程随机生成的树的每个分支满足ω-正则规范？主要结果是，对于LTL规格这个问题是在PSPACE，包含经典的结果，分别为过渡系统和马尔可夫链。底层的一般模型检查算法是基于自动机理论的方法，使用明确的Büchi自动机。
2021-07-04 cs.FL cs.LO
Timed Automata Robustness Analysis via Model Checking
本文针对时间自动机在设计阶段因时间常数不确定及实现扰动导致规范违反的问题，提出了通过模型检查进行鲁棒性分析的概念与技术，以辅助修复模型并确保可达性与安全规范。
2022-07-28 cs.FL cs.LO
Trace-Checking CPS Properties: Bridging the Cyber-Physical Gap
网络物理系统结合了软件和物理组件。规范驱动的CPS跟踪检查工具通常为用户提供一种规约语言来表达感兴趣的需求，并提供一个自动过程来检查这些需求是否保持CPS的执行跟踪。尽管存在用于CPS的若干规约语言，但它们通常不足以表达与软件和物理组件及其交互相关的复杂CPS属性的规范。在本文中，我们提出了（一）混合逻辑信号（HLS），一个基于逻辑的语言，允许复杂的CPS要求的规范，和（ii）TheEodorE，一个有效的SMT为基础的跟踪检查程序。这个过程减少了在执行跟踪上检查CPS需求的问题，检查SMT公式的可满足性。我们评估了我们的贡献，使用一个有代表性的工业案例研究在卫星领域。我们通过考虑我们案例研究的212个要求来评估HLS的表达能力。HLS可以表达所有212个需求。我们还通过运行747个跟踪要求组合的跟踪检查程序来评估TheEodorE的适用性。在74.5%的案件中，EodorE能够做出判决。最后，我们比较了HLS和TheEodorE与其他规约语言和跟踪检查工具的文献。我们的研究结果表明，从实用的角度来看，我们的方法提供了一个更好的表现力和性能之间的权衡。
2021-09-15 cs.FL cs.LO cs.SE
Teaching the Formalization of Mathematical Theories and Algorithms via the Automatic Checking of Finite Models
在逻辑和证明的实际应用中的教育，如计算机程序的形式规范和验证，受到了这样一个事实的严重阻碍，即投入在证明上的大多数时间和精力实际上是徒劳的：由于学生开发的规范和算法中的错误，他们的证明努力往往毫无意义（因为被证明的命题实际上是不感兴趣的）或先验注定要失败的（因为要证明的命题实际上并不成立），这是一个常见的挫折来源，并给形式方法带来了坏名声。RISCAL（RISC算法语言）是一种形式化的规约语言和相关的软件系统，它试图通过使逻辑形式化变得有趣而不是负担来克服这个问题。为此，RISCAL允许学生通过自动评估/执行和检查（小）有限模型来轻松验证命题实例的正确性。因此，许多/大多数错误可以被快速检测到，随后的证明尝试可以集中在更有意义和真实的命题上。
2018-03-05 cs.LO
Abstraction for Epistemic Model Checking of Dining Cryptographers-based Protocols
本文描述了一个抽象的协议，是基于多轮的Chaum的用餐密码协议。证明了这种抽象在知识逻辑中保留了丰富的规范，包括描述一个主体对其他主体知识的了解的规范。该结果可用于优化基于Dining Cryptographers协议的模型检验，并应用于基于知识的程序实现和验证方法中。这样的应用程序的一些案例研究给出了一个协议，使用的用餐密码协议作为一个原始的匿名广播系统。给出了该协议的具体模型和抽象模型的模型检验性能结果，并得出了一些新的结论。
2010-10-12 cs.FL cs.LO
OCTAL: Graph Representation Learning for LTL Model Checking
Purdue University（普渡大学）
针对传统符号模型检测的状态空间爆炸问题，提出基于图表示学习的OCTAL框架，将LTL模型检测转化为二分类任务，实现了显著的准确率与最高11倍的整体加速。
2023-08-19 cs.AI cs.LO cs.SE
Monitoring and Verification of Multitenant Kubernetes Clusters using TLA+ Trace Checking
Faculty of Informatics West University Timi s oara Romania
本文提出一种基于TLA+轨迹检查的监控工具，可从Kubernetes审计日志推断行为并检测多租户等违规，将形式化推理融入实时Kubernetes环境以提升监控与正确性检查效果。
2026-09-28 cs.DC cs.LO
Model Checking for Fragments of Halpern and Shoham's Interval Temporal Logic Based on Track Representatives
模型检验允许人们根据系统行为的形式模型（通常是Kripke结构）自动验证系统预期属性的规范。基于点的时态逻辑，如LTL、CTL和CTL*，描述了系统如何逐状态演化，通常用作规约语言。他们证明自己在各种应用领域相当成功。然而，属性约束的时间顺序的时间扩展的事件，以及涉及时间聚合，这是固有的间隔为基础的属性，不能正确地处理它们。区间时态逻辑（ITLs），以间隔作为其原始的时间实体，原来是非常适合的规范和验证的间隔计算属性（我们解释的所有轨道的Kripke结构作为计算间隔）。研究了Halpern和Shoham的时间区间模态逻辑（HS）的部分片段的模型检验问题。HS的特点是每对区间之间的每种可能的排序关系（所谓的艾伦关系）都有一种模态。首先，我们描述了一个EXPSPACE模型检验算法的HS片段的艾伦的关系满足，满足，开始，开始，和完成，它利用的可能性找到，为每个轨道（无限长），一个等效的有界长度的轨道代表。在检查属性时，它只需要考虑长度不超过给定界限的轨迹。我们证明了这样一个片段的模型检验问题是PSPACE困难的。最后，我们确定了其他表现良好的HS片段，这些片段的表达能力足以捕捉系统的有意义的区间特性，如互斥，状态可达性和非饥饿，其复杂性小于或等于LTL。
2017-09-06 cs.LO
SMT-based Verification of LTL Specifications with Integer Constraints and its Application to Runtime Checking of Service Substitutability
在基于服务的应用程序的执行过程中出现的一个重要问题涉及确定是否可以用具有不同接口的服务来替换正在运行的服务的能力，例如，如果前者不再可用。标准有界模型检验技术可用于执行此检查，但它们必须能够非常快速地提供答案，以免检查妨碍应用程序的可操作性，而不是帮助它。当考虑会话服务时，问题变得更加复杂，即，服务，公开其中具有输入/输出数据依赖关系的操作。在本文中，我们介绍了一个形式化验证技术的线性时序逻辑，允许用户在公式中的整数变量的约束的扩展。这种技术适用于会话服务的可替代性问题被证明是相当快，比现有的内存占用更小。
2010-04-16 cs.LO cs.SE
L2C2: Logic-based LSC Consistency Checking
实时序列图（LSC）已被提出作为一个基于对象间的规范和反应式系统的可视化程序设计语言。在本文中，我们引入了一个基于逻辑的框架来检查LSC规范的一致性。一个LSC模拟器已经在逻辑编程中实现，利用记忆化的深度优先搜索策略，以显示LSC中的反应系统将如何响应一组外部事件序列。定义了一个正式的符号来指定外部事件序列，用并行运算符和测试控件扩展了正则表达式。并行运算符允许在LSC中同时测试交织的并行外部事件;而测试控件为用户提供了一种新的方法来指定和测试某些时间属性（例如，CTL公式）。我们的框架还提供了一个状态转换图或故障跟踪证明一致性检查结果。
2010-02-16 cs.LO
Model Checking Probabilistic Operator Precedence Automata
TU Wien（维也纳工业大学）；AIT Austrian Institute of Technology（奥地利技术研究院）
本文针对概率下推自动机，引入概率算子优先级自动机，并针对POTLf$\chi$规范开发了最优的EXPTIME/EXPSPACE概率模型检测算法，同时支持LTL规范，为递归概率程序验证提供了首个最优上下文无关逻辑。
2026-09-23 cs.LO cs.PL
Constraint-Based Deadlock Checking of High-Level Specifications
在形式化方法的许多应用中，确定没有死锁是很重要的。模型检验用于发现形式化模型中的死锁的使用通常是有限的。在本文中，我们提出了一个基于约束的方法来寻找死锁采用ProB约束求解器。我们提出的一般技术，以及各种改进，必须进行ProB的Prolog内核，如具体化的成员资格和算术约束。这项工作是由一个工业案例研究指导的，博世的一个团队正在对巡航控制系统进行建模。在这个案例研究中，ProB能够快速找到非常大的无死锁约束的反例。在本文中，我们还介绍了这种新技术的其他成功应用。使用SAT和SMT求解器对这些约束的实验迄今为止是不成功的。
2011-09-09 cs.LO cs.PL cs.SE
Symbolic Simulation-Checking of Dense-Time Systems
直观地说，一个（实现）自动机被一个（规范）自动机模拟，如果实现自动机的每个外部可观察的转换也可以由规范自动机完成。在这项工作中，我们提出了一个符号算法的时间自动机的模拟检查。我们首先提出了一个模拟检查程序，操作状态空间，表示与凸多面体，时间自动机。然后，我们提出的技术来表示这些中间结果凸多面体的区域，并使该过程的算法。然后，我们讨论如何在实现自动机中处理芝诺状态。最后，我们完成了算法的实现，并在实验中报告了我们的算法的性能。
2006-10-13 cs.LO cs.SE
Simulating and model checking membrane systems using strategies in Maude
本文提出利用 Maude 策略语言及其模型检测器，将膜系统规范转换为由策略控制的重写理论，从而简化膜系统的模拟与验证。
2024-01-15 cs.LO
Model checking strategy-controlled systems in rewriting logic
本文针对 Maude 内置 LTL 模型检测器无法验证策略控制规约的问题，提出策略感知扩展，并结合表达力分析、应用示例和性能比较验证其有效性。
2024-01-15 cs.LO
Scenario-Based Compositional Statistical Model Checking for Safety Specifications
University of California, Berkeley（加州大学伯克利分校）
针对安全关键系统中组合场景验证成本高的问题，提出基于场景的组合式统计模型检验框架，通过分解场景与规范、独立验证及重要性采样和核密度估计组合结果，实现高效准确验证并降低模拟成本。
2026-10-06 cs.AI cs.LO cs.RO
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
Liveness of Parameterized Timed Networks
研究了具有多时钟的参数化离散时间网络形式的无限状态系统的模型检验问题。我们表明，这个问题是可判定的B-或S-自动机的规格。这样的规范是非常有表现力的（他们严格submerga-regular规范），并且很容易表达复杂的活性和安全属性。我们的结果是通过使用对称广播来模拟时间的流逝，并通过解决使用k-wise交会和对称广播通信的非定时过程的参数化系统的模型检验问题而获得的。我们的可判定性证明利用自动机理论，合理的线性规划和几何推理来解决向量加法系统中的某些可达性问题，我们相信这些证明技术将有助于解决相关问题。
2016-09-14 cs.LO
Visual Analysis of Hyperproperties for Understanding Model Checking Results
模型检查器提供用于证明系统的数学模型满足给定规范的算法。如果发生冲突，则返回一个显示错误行为的反例。理解这些反例是具有挑战性的，特别是对于超属性规范，即，将系统的多个执行相互关联的规范。我们的目标是通过我们的HyperVis工具，它提供了给定的模型，规范和反例的交互式可视化，以促进这种反例的可视化分析。在迭代和跨学科的设计过程中，我们开发了可视化解决方案，可以有效地传达模型检验结果的核心方面。具体来说，我们引入二进制值的图形表示，以提高模式识别，颜色编码，以更好地指示相关方面，视觉增强的文本描述，以及广泛的跨视图突出显示机制。此外，通过对反例的潜在因果分析，我们还能够识别导致违规的值，并将这些知识用于改进编码和突出显示。最后，分析人员可以直接在HyperVis中修改超属性和系统的规范，并启动新版本的模型检验。结合起来，这些特性显著地支持分析人员理解导致反例的错误以及迭代所提供的系统和规范。我们使用HyperVis进行了多个案例研究，并在定性反馈会议中与领域专家进行了测试。参与者的积极反馈证实了与基于文本的手册现状相比的显著改进以及该工具在解释超性质方面的价值。
2021-08-08 cs.HC cs.LO
Automated Mapping of UML Activity Diagrams to Formal Specifications for Supporting Containment Checking
业务分析师和领域专家经常使用与技术和平台无关的高级模型来勾画软件系统的行为。开发人员将用技术细节来完善和丰富这些高级模型。因此，随着时间的推移，细化的模型可能会偏离原始模型，特别是当两种模型独立演化时。在这种情况下，我们专注于行为模型;也就是说，我们的目标是确保细化的低级别行为模型符合相应的高级别行为模型。基于现有的形式化验证技术，我们提出包含检查作为一种手段，以评估系统的行为所描述的低级别模型是否满足已指定的高级别同行。主要障碍之一是如何减轻创建行为模型的正式规范以及一致性约束的负担，这是一项手动完成的繁琐且容易出错的任务。本文提出的方法旨在通过将行为模型视为验证输入，并将行为模型自动映射到可直接由模型检查器使用的形式属性和描述上，来缓解上述挑战。我们讨论了我们的方法中的各种挑战，并展示了我们的方法在说明性场景中的适用性。
2014-04-03 cs.LO cs.SE
Conformance Checking of Fuzzy Logs against Declarative Temporal Specifications
Free University of Bozen-Bolzano（波尔扎诺自由大学）；University of Bologna（博洛尼亚大学）；University of Edinburgh（爱丁堡大学）
针对事件数据带不确定性的场景，研究模糊日志与声明式时态规则的一致性检查问题，定义模糊版LTLf、将检查转化为该逻辑的验证问题，并给出基于PyTorch的高效概念验证实现。
2024-06-17 cs.AI cs.LO
Strategies, model checking and branching-time properties in Maude
本文扩展Maude模型检验能力，使其支持策略控制系统上的CTL*和μ-演算分支时间性质验证，并通过通用高效连接集成外部模型检验器并比较其性能。
2024-01-15 cs.LO
Learning Representations Through Contrastive Neural Model Checking
CISPA Helmholtz Center for Information Security（CISPA 欧洲信息安全研究中心）
该研究针对形式化验证领域表示学习探索不足的问题，提出对比神经模型检验CNML方法，通过自监督对比目标将逻辑规范与系统嵌入共享潜在空间，在检索任务上表现优于基线且可迁移泛化，为形式化语言表示学习提供了新目标。
2025-10-03 cs.LG cs.LO
Towards Extracting Explicit Proofs from Totality Checking in Twelf
Edinburgh逻辑框架（LF）是一种依赖类型的λ演算，可用于形式系统的编码。LF的多功能性允许规范也被构造关于编码系统。该系统利用公式和类型之间的对应关系，在LF中给出逻辑编程解释的规范。通过将特定参数解释为输入，将其他参数解释为输出，规范可以被视为描述非确定性函数。如果特定的这样的函数可以被证明是全的，它们代表了编码系统的元定理的构造性证明。BASINF提供了一套用于建立整体性的工具。然而，所有元定理的证明都是隐式的：Beself的整体性检查并不能产生一个可以给证明检查器的证书。我们从这里开始明确这些证明的过程。我们对待的限制性情况下，在CNOMF的上下文定义（规则的世界）和引理不使用。在这种情况下，我们描述和证明正确的翻译的步骤，在总体检查到一个实际的证明，在同伴逻辑M2。我们打算从长远来看，我们的翻译扩展到所有的Biblaf，并使用这项工作的基础上生产的相关阿贝拉系统的证明。
2013-07-05 cs.LO cs.PL
Logics and Algorithms for Hyperproperties
本文针对需分析多执行路径关系的超性质系统需求，梳理了近十年用于超性质规约的各类逻辑，以及可满足性检查、模型检验等相关算法的研究现状。
2025-01-14 cs.LO
Theorem and Algorithm Checking for Courses on Logic and Formal Methods
RISC算法语言（RISC Algorithm Language，RISCAL）是一种对理论和算法进行形式化建模的语言。RISCAL规范描述了一个无限类的模型，每个模型都有有限的大小;这允许在这样的模型中完全自动地检查所有定理的有效性和所有算法的正确性。因此，RISCAL使我们能够在试图证明整个类的普遍真理之前，快速验证/证伪模型类的样本实例中的命题的特定真理：第一个可以以全自动的方式实现，而第二个通常需要我们的帮助。RISCAL主要是为教育目的而开发的。为此，本文报告了一些新的增强工具：自动生成的可检查的验证条件的算法，可视化的程序的执行和公式的评价，说明计算其结果，并生成基于Web的学生练习和作业从RISCAL规范。此外，我们报告我们的第一次经验与RISCAL在逻辑和正式方法的课程教学，并进一步计划使用这一工具，以加强正规教育。
2019-04-01 cs.LO
Constraint-Driven Modeling Enabling Dual Model Checking and Simulation for Discrete Event Systems
Arizona State University（亚利桑那州立大学）
本文提出Constraint-DEVS方法，扩展DEVS-Suite框架以支持离散事件系统的仿真与模型检查，开发并验证了片上网络模型，为该框架的混合引擎提供了设计制品。
2026-08-25 cs.AR cs.LO cs.SE
Formal Specification and Verification of Fully Asynchronous Implementations of the Data Encryption Standard
本文提出了两种形式化模型的数据加密标准（DES），第一个使用国际标准LOTOS，第二个使用最近的过程演算LNT。两种模型都以异步电路的方式对DES进行编码，即，DES算法的数据流块由经由会合通信的进程表示。为了确保模型的正确性，已经应用了几种技术，包括模型检验，等价性检验，并将从正式模型自动生成的原型产生的结果与DES的现有实现进行比较。模型的完整代码作为附录提供，也可以在CADP验证工具箱的网站上获得。
2015-11-13 cs.CR cs.LO
Neural Model Checking
University of Birmingham（伯明翰大学）；Amazon Web Services（亚马逊网络服务）；Queen Mary University of London（伦敦大学玛丽皇后学院）
本研究提出结合机器学习与符号推理的神经模型检验方法，以神经网络为线性时序逻辑的形式化证明证书，经无监督训练和符号验证实现可靠的硬件形式化验证，性能优于现有主流模型检验工具。
2024-10-31 cs.LG cs.LO
Semiring-based Specification Approaches for Quantitative Security
我们的目标是提供不同的半环为基础的正式工具的规格的安全要求：我们定量地提高了开放系统的方法，根据该系统是部分指定的。因此，我们假设存在一个未知的，可能是恶意的代理，与系统并行交互。两个规范框架沿着两条不同（但仍然相关）的路线设计。首先，通过比较一个系统的行为与预期的，或通过检查这样的系统是否满足一些安全要求：我们研究了一种新的近似行为等价比较进程的行为，从而扩展了广义非演绎成分（GNDC）的方法与分数。作为第二个结果，我们配备了一个模态逻辑与半环值的目的有一个权重相关的满足公式，指定一些要求的属性。最后，我们概括了经典的部分模型检查功能，我们将其命名为定量部分模型检查，以这种方式指出系统必须满足的必要和充分条件，以便被认为是安全的，相对于一个固定的安全/功能阈值。
2015-09-29 cs.CR cs.FL cs.LO
Verifying Verified Code
Chong等人最近在AWS的一个案例研究中提出了一种有效的工业界有界模型检验方法。在本文中，我们报告了一个后续的案例研究，从三个研究问题的角度探讨了方法：（a）证明工件可以跨验证工具使用;（b）验证代码中是否存在错误;（c）规范是否可以改进。为了研究这些问题，我们将$\texttt{aws-c-common}$库的验证任务移植到SEAHORN和KLEE。我们展示了使用编译器语义和交叉检查规范与不同的验证技术的好处，并呼吁标准化证明库扩展，以增加规范的重用。讨论的核查任务可在网上公开查阅。
2021-07-01 cs.LO cs.SE
Model Checking Paxos in Spin
我们提出了一个正式的分布式共识算法模型，在可执行的规约语言Promela扩展了一种新类型的警卫，称为计数警卫，需要实现过渡，依赖于多数表决。我们的形式化利用的抽象，从减少定理适用于特定的案例研究。我们应用模型检查自旋自动验证模型的有限实例，并提取的协议的选举阶段中使用的法定人数的大小的先决条件。
2014-08-26 cs.DC cs.DM cs.LO
On the Complexity of Rational Verification
Monash University（莫纳什大学）；University of Kaiserslautern（凯泽斯劳滕大学）；Sapienza University of Rome（罗马第一大学）；University of Oxford（牛津大学）
理性验证是指检查并发多智能体系统的时间逻辑属性的问题，假设系统中的代理选择形成博弈论均衡的策略。理性验证可以被理解为多智能体系统的模型检验的对应物，但是虽然经典的模型检验可以在多项式时间内完成一些时态逻辑规约语言，如CTL，多项式空间与LTL规范，理性验证要困难得多：理性验证的关键决策问题是2 EXPTIME-完全与LTL规范，即使使用显式状态系统表示。在此背景下，我们在本文中的贡献是三方面的。首先，我们表明，合理验证的复杂性可以大大降低限制规格GR（1），一个片段的LTL，可以代表一个广泛的和实际有用的一类反应系统的响应特性。特别是，我们表明，对于一些相关的设置，合理的验证可以在多项式空间，甚至在多项式时间。其次，我们提供了改进的复杂性结果，合理的验证时，考虑球员的目标给出的平均回报效用函数，可以说是最广泛使用的方法，在并发和多智能体系统的定量目标。最后，我们考虑了满足社会福利约束的计算结果的问题。为此，我们考虑功利主义和平等主义的社会福利，并表明计算这样的结果是PSPACE完全或NP完全。
2022-07-06 cs.AI cs.LO cs.MA
