MAS交互协议的形式化描述和验证  

Formal Description and Verification of MAS' Interaction Protocol

作　　者：陈宏兵[1] 杨群[1] 李千目[1] 许满武[1] 

机构地区：[1]南京大学软件新技术国家重点实验室,南京,210093 南京大学软件新技术国家重点实验室,南京,210093 京理工大学计算机科学与技术系,南京,210094 南京大学软件新技术国家重点实验室,南京,210093

出　　处：《计算机研究与发展》2006年第z1期28-33,共6页Journal of Computer Research and Development

基　　金：江苏省科技攻关计划基金项目(BE2003064)

摘　　要：在MAS的分析与设计中,Agent间的交互协议设计是极其重要的内容.特别是交互协议的正确性、有效性和可验证性尤为关键,因此形式化描述和验证多Agent的交互协议非常有必要.定义了用于描述多Agent基于对话的交互协议的一个演算,该演算是基于进程代数的并且独立于Agent的推理过程.该机制可以实现异构多Agent系统的交互协议验证.通过Agent会话环境的状态和演算的形式语义,可以验证会话协议的一些属性,例如:终止性、是否死锁等.该方法可以有效地解决交互协议的语义验证问题,因为协议的状态和Agent的行为由协议本身定义,并且可以避免基于状态搜索的状态空间爆炸问题.

关 键 词：交互协议 多AGENT 对话协议 Π演算 

分 类 号：TP391[自动化与计算机技术—计算机应用技术]