责任政策形式化验证方法

• 作者: 张涛 谢红 黄少滨
• 来源期刊: 哈尔滨工程大学学报
• 学科: 工学
• 关键词: 多Agent系统 形式化方法 政策建模 社会承诺 模型检测 责任政策
• 年，卷（期）: 2016,（4）
• 页码范围: 585-591
• 页数: 7页
• 分类号: TP311.5
• 字数: 8282字
• 语种: 中文
• DOI: 10.11990/jheu.201501007

摘要

为了验证多Agent系统设计的正确性，将责任政策作为约束多Agent交互行为的高层“需求规格”或“通信协议”，对其进行形式化建模及验证。研究了建模责任政策的形式化框架语言，基于责任状态模型建模责任政策的动态演化过程。给出了政策模型形式化验证方法，将政策模型的操作语义定义为Kripke 结构的状态迁移系统，政策中Agent行为的约束规则声明为线性时序逻辑公式，使用模型检测器NuSMV验证政策模型对线性时序逻辑公式的可满足性。实验结果表明，该方法可有效分析责任政策的设计缺陷，提高多Agent系统设计的正确性。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	谢红	哈尔滨工程大学信息与通信工程学院	134	692	14.0	19.0
2	张涛	哈尔滨工程大学计算机科学与技术学院	85	1098	19.0	31.0
6	黄少滨	哈尔滨工程大学计算机科学与技术学院	55	319	10.0	15.0