%0 Journal Article
%T 责任政策形式化验证方法
%A 张涛
%A 谢红
%A 黄少滨
%J 哈尔滨工程大学学报
%D 2016
%R 10.11990/jheu.201501007
%X 为了验证多Agent系统设计的正确性,将责任政策作为约束多Agent交互行为的高层"需求规格"或"通信协议",对其进行形式化建模及验证。研究了建模责任政策的形式化框架语言,基于责任状态模型建模责任政策的动态演化过程。给出了政策模型形式化验证方法,将政策模型的操作语义定义为Kripke结构的状态迁移系统,政策中Agent行为的约束规则声明为线性时序逻辑公式,使用模型检测器NuSMV验证政策模型对线性时序逻辑公式的可满足性。实验结果表明,该方法可有效分析责任政策的设计缺陷,提高多Agent系统设计的正确性。
%K 多Agent系统
%K 形式化方法
%K 政策建模
%K 社会承诺
%K 模型检测
%K 责任政策
%U http://heuxb.hrbeu.edu.cn/oa/darticle.aspx?type=view&id=201501007