多智能体系统时态认知规范高效符号模型检测的算法研究

• 作者: 吴立军 苏开乐 苏金树
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: OBDDs mu演算 时态认知逻辑 符号模型检测 安全协议验证
• 年，卷（期）: 2008,（2）
• 所属期刊栏目: 研究论文
• 页码范围: 245-252
• 页数: 8页
• 分类号: TP18
• 字数: 7357字
• 语种: 中文
• DOI: 10.3321/j.issn:0254-4164.2008.02.008

摘要

Clarke和McMillan提出了利用mu演算和OBDDs符号模型检测时态逻辑的方法.这些方法是非常有效的,能用于验证许多具有极大状态空间的实际系统(状态个数可以超过1020).但是,这些方法不能检测知识逻辑.而时态认知逻辑能更精确地描述分布式领域中系统和协议的规范.文章首先讨论了Kripke结构和mu演算的扩展,然后提出了利用扩展mu演算和OBDDs符号模型检测时态认知逻辑的方法.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	苏开乐	中山大学计算机科学与技术系	22	309	11.0	17.0
2	苏金树	国防科学技术大学计算机学院	64	1757	15.0	41.0
3	吴立军	国防科学技术大学计算机学院	2	13	2.0	2.0