| 责任政策形式化验证方法 |
| |
| 引用本文： | 张涛,谢红,黄少滨.责任政策形式化验证方法[J].哈尔滨工程大学学报,2016(4):585-591. |
| |
| 作者姓名： | 张涛 谢红 黄少滨 |
| |
| 作者单位： | 哈尔滨工程大学计算机科学与技术学院;哈尔滨工程大学信息与通信工程学院 |
| |
| 基金项目： | 国家科技支撑计划(2012BAH08B02);中央高校基本科研业务费专项基金项目(HEUCF100603,HEUCF041204);黑龙江省博士后基金资助项目(3236310148) |
| |
| 摘 要： | 为了验证多Agent系统设计的正确性,将责任政策作为约束多Agent交互行为的高层"需求规格"或"通信协议",对其进行形式化建模及验证。研究了建模责任政策的形式化框架语言,基于责任状态模型建模责任政策的动态演化过程。给出了政策模型形式化验证方法,将政策模型的操作语义定义为Kripke结构的状态迁移系统,政策中Agent行为的约束规则声明为线性时序逻辑公式,使用模型检测器Nu SMV验证政策模型对线性时序逻辑公式的可满足性。实验结果表明,该方法可有效分析责任政策的设计缺陷,提高多Agent系统设计的正确性。
|
| 关 键 词： | 多Agent系统 形式化方法 政策建模 社会承诺 模型检测 责任政策 |
| 本文献已被 CNKI 等数据库收录！ |
|
