多智体系统时态认知规范的模型检测算法

摘要：

模型检测技术一直以来主要是检验用时态逻辑描述的规范,人们很少注意认知逻辑的模型检测问题,而在分布式系统领域,系统和协议的规范已广泛地采用知识逻辑来描述.着重研讨了时态认知逻辑的模型检测算法.在SMV(symbolic model verifier)模型检测器的基础上,根据知识的语义和集合理论,提出了多种检验知识和公共知识的算法,从而使SMV的检测功能由时态逻辑扩充到时态认知逻辑.这些方法也适用于其他以状态集合作为输出的模型检测方法和工具的功能扩充.

关键词：符号模型检测、多智体系统、协议验证、SMV、TMN密码协议

所属期刊栏目：15

分类号：TP18(自动化基础理论)

资助基金：国家自然科学基金60073056;广东省自然科学基金001174

在线出版日期：2004-08-12（万方平台首次上网日期，不代表论文的发表时间）

页数：共9页

页码：1012-1020