张 涛，谢 红，黄少滨



多Agent交互策略模型检测方法

张 涛1,2，谢 红2，黄少滨1

(1. 东北农业大学电气与信息学院 哈尔滨 150030；2. 哈尔滨工程大学信息与通信工程学院 哈尔滨 150001)

提出一种基于模型检测的多Agent交互策略验证方法，首先通过责任政策语言建模多Agent的交互策略，基于责任政策语言的操作语义将政策模型转换为模型检测器NuSMV的输入，利用时态逻辑声明表征策略冲突的系统性质，然后利用模型检测器NuSMV自动验证政策模型对性质的可满足性，并根据模型检测器产生的反例分析交互策略中的各种错误。该方法可提高交互策略的验证效率，确保多Agent系统设计的正确性。

形式化方法; 模型检测; 多Agent系统; NuSMV; 政策建模

多Agent系统中，责任一般是Agent为了满足某些要求而执行的动作[1]，如“社会保障管理条例规定企业在成立之日起的20个工作日内，需持营业执照到当地社会保险经办机构办理社会保险登记”。责任或是Agent被要求保持的某种状态[2]，如“养老保险缴费人员必须处于参保状态”。责任政策约束其所属领域内Agent间的交互行为，可被视为系统设计中的高层“需求规格”或“交互策略”[3]。在多Agent系统中，建模和验证多Agent间的交互策略有助于正确设计Agent间的交互行为，提高系统的正确性和可靠性[4]。文献[5]在计算机科学领域提出研究规律政策的观点，文献[6]开创了关于分布式系统中的政策研究方向，并提出了“规律控制的交互(law-governed interaction, LGI)”，由此激发了该领域的深远研究与大量实践工作。尽管LGI模型曾被成功用于多Agent系统的各种研究与应用领域，但该模型使用低层抽象信息描述系统中的交互行为，使其逐渐不能满足复杂系统的设计需求。……