| 多Agent交互策略模型检测方法 |
| |
| 引用本文： | 张涛,谢红,黄少滨.多Agent交互策略模型检测方法[J].电子科技大学学报（自然科学版）,2016,45(5):802-807. |
| |
| 作者姓名： | 张涛 谢红 黄少滨 |
| |
| 作者单位： | 1.东北农业大学电气与信息学院 哈尔滨 150030 |
| |
| 基金项目： | 国家科技支撑计划2012BAH08B02中央高校基本科研业务费专项基金HEUCF100603，HEUCF041204黑龙江省博士后资助项目3236310148 |
| |
| 摘 要： | 提出一种基于模型检测的多Agent交互策略验证方法，首先通过责任政策语言建模多Agent的交互策略，基于责任政策语言的操作语义将政策模型转换为模型检测器NuSMV的输入，利用时态逻辑声明表征策略冲突的系统性质，然后利用模型检测器NuSMV自动验证政策模型对性质的可满足性，并根据模型检测器产生的反例分析交互策略中的各种错误。该方法可提高交互策略的验证效率，确保多Agent系统设计的正确性。
|
| 关 键 词： | 形式化方法 模型检测 多Agent系统 NuSMV 政策建模 |
| 收稿时间： | 2015-01-12 |
The Method of Model Checking Policy of Multi-Agent Interaction |
| |
| Affiliation: | 1.School of Electrical and Information, Northeast Forestry University Harbin 1500302.College of Information and Communication Engineering, Harbin Engineering University Harbin 150001 |
| |
| Abstract: | A verification method of multi-agent interaction policy is proposed based on model checking. The model of system is specified with obligation policy language and it is converted to the input model of model checker NuSMV based on its operational semantics, the properties of system depending on different types of policy conflicts are represented with temporal logic, and the violations of properties are detected by using NuSMV model checker, which can provide the counterexample and trace it back to the errors in interaction policy. The result shows that the method can improve the efficiency of verifying interaction policy, and it ensures the correctness of the design of Multi-Agent systems. |
| |
| Keywords: | |
|
| 点击此处可从《电子科技大学学报（自然科学版）》浏览原始摘要信息 |
|
点击此处可从《电子科技大学学报（自然科学版）》下载全文 |
