Jul, 2022

多智能体系统的运行时验证

PDF
TL;DR本文提出了一种运行时验证（RV）方法，使用 JaCaMo 框架实现对多主体系统（MAS）的安全控制，以防止自然语言对话流程中的话题改变影响 MAS 的推理过程。并演示通过该方法可以帮助医院床位分配方面做决策。
发现论文，激发创造
  • 可重构的 MAS 建模交互

    我们提出了一种形式化模型来描述和推理多智能体系统，允许代理以不同的模式进行交互和通信，定义了基于共享变量的本地行为和基于消息传递的全局行为，并扩展了线性时态逻辑 (LTL) 以明确推理不同代理的意图和交互协议，研究了扩展的可满足性和模型检测的复杂性。

    Jun, 2019

  • 基于 Agent 的自主系统决策实际验证

    本文介绍了一种验证方法，用于分析基于代理的混合系统中的决策制定组件，该方法包括适用于基于代理的逻辑组件的模型检查技术，并且该技术与连续部分的混合系统的单独分析相结合，从而允许使用程序模型检查器来验证混合自主系统中决策制定的实际实现。

    Oct, 2013

  • 多智能体验证与控制的概率模型检验

    概率模型检查是一种在不确定性或随机性背景下对软件或硬件系统进行形式化自动推理的技术。该技术综合了来自多个领域的思想和技术，包括逻辑、自动机理论、图论、优化、数值方法和控制。最近，概率模型检查还扩展到整合博弈论中的思想，特别是使用随机博弈模型和均衡解概念来正式验证具有不同目标的多个理性代理之间的交互。这提供了一种灵活推理有关代理以对抗或协作方式行动的手段，并为人工智能、机器人和自主系统等领域解决新问题带来机遇。本文概述了该领域的一些进展，并强调了它们已经被使用的应用。我们讨论了概率模型检查的优势如何应用或有潜力应用于多智能体系统，并概述了在这一领域取得更进一步的关键挑战。

    Aug, 2023

  • 动态多智体系统的分层控制器综合

    该论文针对多智能体控制问题提出了分层方法，其中包括三个阶段：计算系统的高级计划、通过 SMT 公式处理组合问题，以及使用强化学习获得神经网络控制策略，由于其正确性具有构建性，但缺乏实时执行功能，因此使用 SWA-SMT 解决方案作为最后阶段的初始训练数据集

    Jul, 2023

  • 多视角信息认证实现的强韧性多智能体通信

    本文提出了一种名为 CroMAC 的多智能体通信安全策略，并使用多视角自动编码器将所有信息提取出来进行证书验证，在多个协作多智能体基准测试中，证明了 CroMAC 的有效性。

    May, 2023

  • 具有空间 - 时间感知能力的安全多智能体强化学习：应对复杂场景下的联网自动驾驶车辆

    本文提出了一种使用多智能体强化学习框架 (MARL) 的安全保护平行体系结构来提高连接和自主车辆 (CAV) 系统在复杂驾驶情况下的安全性和效率，并使用 Graph Convolutional Network (GCN)-Transformer 作为空间 - 时间编码器，设立安全屏障并对 CAV 进行安全检查，实验结果显示该方法大大提高了系统安全性和效率。

    Oct, 2022

  • 自动化生成用于自动驾驶系统系统级仿真验证的场景

    基于 CARLA 和 ScenarioRunner 的系统级仿真验证验证框架的实例化研究，以及其在自动驾驶系统的自动生成场景方面的有效性研究。

    Nov, 2023

  • 自主机器人的鲁棒验证的贝叶斯学习

    利用 Bayesian learning 的框架进行 runtime verification，以验证在不确定环境中执行的关键任务的自主机器人，将这些方法应用于水下基础设施的检查和维修的自主机器人任务的验证案例研究中。

    Mar, 2023

  • 验证学习为基础的安全关键航空系统的认证框架

    本文提出了一种针对航空系统中基于学习的组件进行设计时间和运行时保证的安全验证框架，该框架整合了两种新方法：同时考虑了离线和在线验证机制，并且允许各个模块使用独立的方法和技术进行开发，以满足系统不同阶段的安全性要求，从而实现系统产品的持续学习和评估。

    May, 2022

  • 基于组件的建模与仿真检验框架：集成各组件

    本文提出了一个综合的验证框架来应对组合性验证中的一些重要问题，并提出了一个验证过程来验证不同类型的系统模型，如反应式、实时和概率系统的组合性。该框架提供了验证组合性所需的方法、技术和工具支持。为了验证动态 - 语义组合性，我们探讨了三种不同的方法，即基于 Petri 网的代数分析、基于有色 Petri 网的状态空间分析和基于通信顺序处理的模型检查。

    Jan, 2023