责任政策形式化验证方法

作     者：张涛 谢红 黄少滨 ZHANG Tao;XIE Hong;HUANG Shaobin

作者机构：哈尔滨工程大学计算机科学与技术学院黑龙江哈尔滨150001 哈尔滨工程大学信息与通信工程学院黑龙江哈尔滨150001 

基　　金：国家科技支撑计划(2012BAH08B02) 中央高校基本科研业务费专项基金项目(HEUCF100603 HEUCF041204) 黑龙江省博士后基金资助项目(3236310148) 

出 版 物：《哈尔滨工程大学学报》 (Journal of Harbin Engineering University)

年 卷 期：2016年第37卷第4期

页      码：585-591页

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

主 题 词：多Agent系统 形式化方法 政策建模 社会承诺 模型检测 责任政策 

学科分类：0817[工学-轻工类] 08[工学] 0807[工学-电子信息类] 0827[工学-食品科学与工程类] 0802[工学-机械学] 0703[理学-化学类] 0835[0835] 0825[工学-环境科学与工程类] 0811[工学-水利类] 0801[工学-力学类] 081202[081202] 0812[工学-测绘类] 

核心收录：

D　O　I：10.11990/jheu.201501007

馆 藏 号：203128967...