《计算机学报》文章摘要   全文下载
文章题目	多智能体系统时态认知规范高效符号模型检测的算法研究
作者	吴立军1) 苏金树1) 苏开乐2)
作者单位	1)(国防科学技术大学计算机学院 长沙 410073) 2)(中山大学计算机科学与技术系 广州 510275)
发表年份	2008
发表月份	2期(245—252)
文章摘要	摘要 Clarke和McMillan提出了利用mu演算和OBDDs符号模型检测时态逻辑的方法.这些方法是非常有效的，能用于验证许多具有极大状态空间的实际系统(状态个数可以超过1020).但是，这些方法不能检测知识逻辑.而时态认知逻辑能更精确地描述分布式领域中系统和协议的规范.文章首先讨论了Kripke结构和mu演算的扩展，然后提出了利用扩展mu演算和OBDDs符号模型检测时态认知逻辑的方法. 关键词 OBDDs；mu演算；时态认知逻辑；符号模型检测；安全协议验证 中图法分类号 TP18