Formal Verification of Probabilistic Multi-Agent Systems for Ballistic Rocket Flight Using Probabilistic Alternating-Time Temporal Logic
Institute of Computer Science, Polish Academy of Sciences（波兰科学院计算机研究所）；SpaceForest Sp. z o.o.（SpaceForest有限公司）
本研究提出基于概率交替时间时序逻辑的验证方法，用于验证弹道火箭飞行轨迹的安全性，通过整合真实飞行数据和环境随机性分析，确保任务安全并维持科学目标。
2025-11-27 cs.LO cs.MA
Towards the Combination of Model Checking and Runtime Verification on Multi-Agent Systems
针对多智能体系统形式化验证难、模型检测问题通常不可判定的问题，提出结合模型检测与运行时验证的方法，用模型检测器验证可判定片段子模型、运行时监控器验证其余部分，并实现技术验证了效果。
2022-04-19 cs.LO cs.MA
A Rational Agent Controlling an Autonomous Vehicle: Implementation and Formal Verification
在我们的道路上开发和部署自动驾驶汽车（AV）不仅在不久的将来是现实的，而且还可以带来显着的好处。特别是，它可以潜在地解决与车辆和交通有关的几个问题，例如：（i）可能减少交通拥堵，从而提高燃油经济性和减少驾驶员不活动;（ii）可能减少事故数量，假设AV可以最小化经常导致交通事故的人为错误;以及（iii）增加停车的便利性，特别是当人们考虑到共享AV的潜力时。为了部署AV，必须在硬件和软件方面完成一些重要步骤。正如预期的那样，软件组件在复杂的AV系统中起着关键作用，因此，至少为了安全起见，我们应该评估这些组件的正确性。在本文中，我们关注的是负责AV中的决策的高级软件组件。我们打算建立一个AV能够导航，避障，障碍物选择（当碰撞是不可避免的）和车辆恢复等，使用理性的代理。为了实现这一目标，我们建立了以下阶段。首先，代理计划和操作已在Gwendolen代理程序设计语言中实现。第二，我们用Java语言构建了一个模拟的汽车环境。第三，我们通过LTL公式正式指定了一些所需的代理属性，然后使用AJPF验证工具对其进行正式验证。最后，在MCAPL框架内（包括前几个阶段使用的所有工具），我们已经获得了我们的AV代理在其特定行为方面的形式化验证。例如，负责选择具有低潜在损害的障碍物而不是较高损害障碍物（如果可能）的代理计划可以在MCAPL内正式验证。我们必须强调的是，我们目前的方法的主要目标在于代理计划的形…
2017-09-08 cs.LO cs.MA
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
Logic-based Specification and Verification of Homogeneous Dynamic Multi-agent Systems
我们开发了一个基于逻辑的框架，形式化规范和算法验证的同质和动态的并发多代理转换系统（HDMAS）。同质性意味着所有的代理在任何给定的状态下都有相同的可用动作，并且这些动作具有相同的效果，而不管是哪个代理执行它们。因此，状态转换仅由执行每个动作的主体的数量的向量确定，并且通过在Presburger算术中可定义的这些数量的条件来象征性地指定。代理分为可控（由系统管理员/控制器）和不可控，代表环境或对手。动态性意味着在整个系统演化过程中，可控和不可控主体的数量可能会发生变化，可能在每次转换时都会发生变化。作为形式化规范的语言，我们使用交替时间时态逻辑（ATL）的适当扩展版本，其中可以指定类型为“（至少）$n$可控代理可以针对（至多）$m$不可控代理确保系统的任何可能的演变满足给定目标$φ$“，其中，$φ$再次被指定为该语言的公式，并且$n$和$m$中的每一个是固定数或可以量化的变量。我们提供了形式语义我们的逻辑$\mathcal{L}_{HDMAS}$和定义范式的公式。证明了$\mathcal{L}_{HDMAS}$中的公式在有限域等价于一个规范型公式，并给出了有限HDMAS模型中范式公式的全局模型检验算法，调用Presburger公式的模型检验真值.我们建立了最坏情况下的复杂性估计的模型检验算法，并说明了它的运行示例。
2020-03-19 cs.LO cs.MA
Contract-based Design and Verification of Multi-Agent Systems with Quantitative Temporal Requirements
本文提出定量假设-保证契约，实现多智能体系统在定量时间逻辑LTL[$\mathcal{F}$]规范下的组合式设计与验证，提高可扩展性和模块化。
2024-12-17 cs.LO
Program Semantics and a Verification Technique for Knowledge-Based Multi-Agent Systems
我们给出了“基于知识的程序”的关系和最弱前提语义，即，限制变量的可观测性的程序，以便丰富地表达能够或不能观测所述变量的代理的知识的变化。基于这些知识为基础的程序，我们定义了一个程序的认知逻辑模型复杂的认知属性的多智能体系统的执行。我们翻译的有效性程序认知逻辑公式的一阶有效性，使用我们最弱的前提语义和巧妙的簿记变量分配。我们在Haskell中以一般的方式实现我们的翻译（即，独立于逻辑语句中的程序），并在一系列行之有效的例子上测试我们的新程序-认知逻辑的这种新颖的验证方法。
2022-07-06 cs.LO
LTL Verification of Memoryful Neural Agents
Imperial College London（帝国理工学院）
提出针对有记忆神经多智能体系统的LTL验证框架，支持有界与无界规范，通过边界模型检测与约束求解技术，首次实现无界规范验证并大幅提升有界验证效率。
2025-03-04 cs.AI cs.LG cs.LO
Multi-Agent Safety Verification using Symmetry Transformations
我们表明，对称变换和缓存可以实现可扩展的，可能是无界的，多代理系统的验证。对称变换将解和映射到其他解。我们表明，这个属性可以用来转换缓存的可达集计算新的可达集，混合动力和多智能体模型。我们开发了一个虚拟系统的概念，它定义了一个广泛的一类代理模型，访问航点序列的对称变换。使用这个概念的虚拟系统，我们提出了一个原型工具CacheReach，建立一个缓存的reachtubes为这个系统，在某种程度上，是不可知的reachsets和可达性分析子程序的表示。我们的CacheReach的实验评估显示，在多智能体系统的3维线性和4维非线性固定翼飞机模型的航点序列的安全验证计算时间节省了66%。这些节省和我们的理论结果说明了使用基于缓存的多代理系统的安全验证的潜在好处。
2019-11-01 cs.FL cs.LO cs.SC
Composable Verification Pipelines for Multi-Agent Systems
Ume University, Sweden（乌梅大学，瑞典）
研究多智能体系统的验证问题，基于Tiles和Soda构建模块化框架，通过可执行验证管道操作动作语言语义，以类型化函数管道表示验证过程，含可执行规范层，有开源实现及示例说明。
2026-07-21 cs.AI cs.LG cs.LO
Agentproof: Static Verification of Agent Workflow Graphs
Luleå tekniska universitet（吕勒奥理工学院）
Agentproof通过提取四个主流代理框架的统一抽象图模型，应用六种结构检查并生成见证轨迹，评估时间安全策略，实现无需手动建模的静态验证，发现工作流中的结构缺陷和政策违规。
2026-03-20 cs.CR cs.FL cs.LO
Automated Temporal Equilibrium Analysis: Verification and Synthesis of Multi-Player Games
Monash University（莫纳什大学）；University of Kaiserslautern（凯泽斯劳滕大学）；Sapienza University of Rome（罗马大学）；University of Oxford（牛津大学）
在多智能体系统的背景下，合理的验证问题是有关检查的时间逻辑属性将在一个系统中举行时，它的组成代理被假定为理性和战略行为，在追求个人目标。通常，这些目标被表示为相关代理希望看到满足的时间逻辑公式。不幸的是，理性验证在计算上是复杂的，并且需要专门的技术来获得实际可用的实现。在本文中，我们提出了这样一种技术。这种技术依赖于减少合理的验证问题的解决方案的一个集合的奇偶校验游戏。我们的方法已在平衡验证环境（EVE）系统中实现。EVE系统作为输入的并发/多代理系统的模型表示使用简单的反应模块语言（SRML），其中代理的目标表示为线性时序逻辑（LTL）公式，连同索赔的平衡行为的系统，也表示为LTL公式。然后，EVE可以检查LTL声明是否对系统的某些（或每个）计算有效，这些计算可能是通过代理选择纳什均衡策略而产生的;它还可以检查系统是否具有纳什均衡，并为多玩家游戏中的玩家合成个人策略。在给出了我们的基本框架之后，我们描述了我们的新技术，并证明了它的正确性。然后，我们描述了我们的EVE系统中的实现，并提出了实验结果表明，EVE表现良好，相比其他现有的工具，支持合理的验证。
2020-08-13 cs.AI cs.GT cs.LO
Synchronous Agents, Verification, and Blame -- A Deontic View
本文面向双智能体同步系统，提出融合义务、许可、禁止与补偿机制的道义逻辑，支持模型检测、违反归责及基于补偿代价的交互定量比较。
2023-09-26 cs.LO
Verification of Agent-Based Artifact Systems
Laboratoire Ibisc, Université d’Evry（埃夫里大学Ibisc实验室）；Imperial College London（帝国理工学院）；Università di Roma “La Sapienza”（罗马大学（萨皮恩扎））
人工智能系统是一种新颖的范例，用于指定和实现业务流程，这些业务流程用称为工件的交互模块来描述。工件由数据和生命周期组成，分别说明工件状态的关系结构和它们随时间的可能演变。在本文中，我们提出了以人为中心的多智能体系统，一种新的形式化的工件系统的背景下，多智能体系统对他们进行操作。与通常的基于流程的服务模型不同，我们给出的语义明确地说明了工件系统所定义的数据结构。我们研究的模型检验问题，以人为中心的多智能体系统对规范写在一个量化的版本的时间认知逻辑表示的代理人的知识在交流。我们首先注意到，这个问题一般是不可判定的。然后，我们确定了两个值得注意的限制，一个语法和语义，使我们能够找到bisilimeric有限的抽象，从而减少有限模型的实例上的模型检验问题。在这些假设下，我们证明了这些系统的模型检验问题是EXPSPACE完全的。然后，我们介绍了以人为中心的程序，紧凑和声明性表示的程序管理的工件系统和代理。我们表明，虽然这些原则上产生无限状态系统，在自然条件下，他们的验证问题可以解决有限的抽象，可以有效地计算程序。最后，我们通过一个主流的采购方案，从工件系统文献的理论结果的文件。
2013-01-22 cs.AI cs.LO cs.MA
Verification of agent knowledge in dynamic access control policies
我们开发了一种基于解释系统的建模技术，以验证访问控制策略的时间认知属性。这种方法使我们能够检测信息流的动态策略中的漏洞，通过验证的知识，通过阅读和推理系统信息的代理。为了克服实际的限制状态爆炸模型检查的时间认知属性，我们引入了一种新的抽象和细化技术的时间认知安全属性在ACTLK（ACTL知识模态K）和一类有趣的属性，不属于这一类。
2014-01-19 cs.CR 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
Formal Verification of Learned Multi-Agent Communication Policies via Decision Tree Distillation
University of Arkansas at Little Rock（阿肯色大学小石城分校）
提出通过决策树蒸馏将多智能体强化学习策略转化为可解释模型，并利用PRISM进行形式化验证，确保安全属性转移至原始网络，在无人机编队任务中实现88.9%属性满足率。
2026-06-19 cs.AI cs.LG cs.LO
Rational Verification for Probabilistic Systems
Monash University（莫纳什大学）；University of Oxford（牛津大学）；University of Kaiserslautern（凯泽斯劳滕大学）
理性验证是确定在多智能体系统中，在系统中的智能体理性行动的假设下，通过选择共同形成博弈论均衡的策略，将持有哪些时间逻辑属性的问题。以前在这方面的工作主要集中在确定性系统。在本文中，我们发展的理论和算法的合理性验证概率系统。我们专注于并发随机游戏（CSG），它可以用来模拟复杂的多智能体环境中的不确定性和随机性。在定性概率环境下，研究了非合作博弈和合作博弈的理性验证问题。在前一种情况下，我们认为LTL性质满足的纳什均衡的游戏，在后一种情况下，LTL性质满足的核心。在这两种情况下，我们表明，问题是2 EXPTIME-完全的，因此不困难比简单得多的验证问题的模型检验LTL性能的系统建模为马尔可夫决策过程（MDPs）。
2021-07-26 cs.AI cs.GT cs.LO
Bridging LLM Planning Agents and Formal Methods: A Case Study in Plan Verification
J.P. Morgan AI Research（摩根大通人工智能研究）
本文提出一种利用大语言模型将自然语言计划转换为形式化逻辑并进行验证的框架，展示了GPT-5在计划验证中的高准确率及形式化表示的生成能力。
2025-11-24 cs.AI cs.LO
FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification
Astrio Labs（阿斯特里奥实验室）
提出 FORALL-LEAN-AGENT 框架，通过隔离工作区、公理审计和独立检查实现可审计的 Lean 证明验证，在 VeriSoftBench 和 PutnamBench 上提升成功率并降低成本。
2026-10-02 cs.AI cs.LO cs.SE
Formal Ethical Obligations in Reinforcement Learning Agents: Verification and Policy Updates
Oregon State University（俄勒冈州立大学）
本文提出期望行为功利主义道义逻辑及两种算法，用于在逻辑层面验证强化学习智能体的伦理义务并修改其策略以满足这些义务，从而提高权衡透明度。
2024-07-31 cs.AI cs.LO
AgentLTL: A Trace-Verification Framework for Measuring, Enforcing, and Training Procedural Compliance in Tool-Using LLM Agents
EPITA；Bpifrance
介绍基于一阶线性时态逻辑的AgentLTL语言，用于表达代理跟踪的程序规则，产生确定性无评判的合规分数，此框架可用于约束和微调，提升模型合规性与准确性。
2026-07-07 cs.AI cs.LO cs.SE
Automating Formal Verification with Agent-Guided Tree Search
Massachusetts Institute of Technology（麻省理工学院）；Department of Electrical Engineering and Computer Science（电气工程与计算机科学系）
本文提出智能体引导的树搜索方法，通过状态和上下文两种编排器改进基于大语言模型的Lean形式验证代码生成性能，在基准测试中达到95.0%的通过率。
2026-05-26 cs.LG cs.LO cs.SE
Parameterized verification of synchronization in constrained reconfigurable broadcast networks
可重构广播网络提供了一个方便的形式主义建模和推理的移动代理广播消息到其他代理的网络以下一些（不断发展的）通信拓扑结构。这些模型的参数化验证旨在检查给定的属性是否与初始配置（代理数量，初始状态和初始通信拓扑结构）无关。我们在这里集中在同步属性，询问是否所有代理收敛到一组目标状态后，一些执行。这个问题是已知的，在多项式时间内，当没有约束的通信拓扑结构的演变（而它是不可判定的静态广播网络）是可判定的。在本文中，我们研究如何重新配置的各种约束影响的可判定性和复杂性的同步问题。特别是，我们表明，当绑定的数量重新配置的链接之间的两个通信步骤由一个常数，同步变得不可判定;另一方面，同步仍然是可判定的PTIME时，绑定的代理数量的增长。
2018-02-23 cs.DC cs.FL cs.LO
