资源描述：
《多智能体系统时态认知规范高效符号模型检测的算法研究_》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。
1、多智能体系统时态认知规范高效符号模型检测的算法研究本课题受国家自然科学基金（90604006，60496327，60496327）和德国科学研究基金（446CHV113/240/0-1）资助。吴立军,男,1965年生，博士后,副教授,主要研究领域为模型检测与网络安全，E-mail:gzzsudocwlj@yahoo.com,联系地址：广州市天河区天平架沙太南路阳光家园A702，电话：020-87233631。苏金树,男,1960年生，教授,博士生导师,主要研究领域为网络安全。苏开乐,男,1964年生，教授,博士生导师,主要研究领域为模型检测与网络安全;.吴立军1，苏金树1，苏开乐21（国防科学
2、技术大学计算机学院，长沙410073）2(中山大学计算机科学与技术系，广州510275)摘要Clarke和McMillan提出了利用mu演算和OBDDs符号模型检测时态逻辑的方法。这些方法是非常有效的，能用于验证许多具有极大状态空间的实际系统（状态个数可以超过1020）。然而，这些方法不能检测知识逻辑。但是时态认知逻辑能更精确地描述分布式领域中系统和协议的规范。这篇文章首先讨论了Kripke结构和mu演算的扩展，然后提出了利用扩展mu演算和OBDDs符号模型检测时态认知逻辑的方法。关键词OBDDs；mu演算；时态认知逻辑；符号模型检测；安全协议验证1引言模型检测自十九世纪八十年代提出以来，已经
3、变成了最成功的自动验证技术之一。它被广泛地应用于硬件测试和通信协议和控制系统的有效性证明等诸多领域。模型检测一直以来主要用来检验系统是否满足用时态逻辑描述的规范。人们很少注意知识逻辑的模型检测的问题。然而在分布式系统中，时态认知逻辑能更准确地描述系统和协议的规范，因而被广泛地用于系统和协议的规范描述。因此模型检测时态认知逻辑是一个新的重要的研究领域。RonvanderMeyden和N.V.Shilov讨论了具有完全记忆的系统中模型检测知识和时间的问题[1]。WiebevanderHoek等提出了基于命题逻辑的时态认知逻辑模型检测算法[2]。但它只是局限于由LTL和知识算子组成的逻辑，而且他们的
4、工作基础还需进一步研究。苏开乐等在时态认知逻辑方面也做了许多工作[3-4]。吴立军等讨论并提出了基于SMV的时态认知逻辑模型检测方法，但没有解决极大状态空间系统的模型检测问题[5]。mu演算是一种功能强大的语言，它通过使用最大最小固定点算子来描述转移系统的性质。许多时态和程序逻辑能转换成mu演算。而mu演算存在高效的模型检测算法。因此研究者们对mu演算在计算机辅助验证领域的应用产生了极大的兴趣。OBDDs(OrderedBinarydecisionDiagrams)是布尔公式的经典表达式。实际上它们比传统的CNF和DNF范式更加紧凑。因此OBDDs被广泛应用于计算机辅助设计和验证中，包括组合逻
5、辑的符号验证等。通过它我们可以验证许多具有极大状态空间的实际系统。而这些系统的验证是状态枚举法无法实现的。Clarke和McMillan等提出了通过mu-演算和OBDDs符号模型检测时态逻辑的方法[9][10]。这些方法具有极高的效率，能用来验证许多具有极大状态空间的实际系统（状态个数超过1020）。然而，这些方法不能模型检测认知逻辑。本文根据以上方法和知识的语义，利用扩展的mu-演算和OBDDs，给出了高效符号模型检测时态认知逻辑的方法（由CTL(ComputationTreeLogic)和知识算子组合而成的时态认知逻辑）。这些方法能够对具有极大状态空间的系统进行安全属性的验证。作为例子，我
6、们给出了SSL2.0的安全属性的验证。2Kripke结构的扩展和mu-演算的扩展2.1Kripke结构的扩展假设Kripke结构M＝（S,T,L），其中S是状态集合，T是转移关系的集合，L是映射L:S®2AP(AP是命题集合)，每一状态对应在该状态下为真的原子命题集合，假设有n个智能体agenti(i=1,2,…,n),且S的任意状态s=(s1,s2,…,sn)，其中si是agenti的局部状态(这里环境也看做一个智能体)，s是系统的全局状态,定义trace是一个有限状态序列u1u2…um(使得对所有07、每一个有限前缀都是一个trace，设s=(s1,s2,…,sn)，t=(t1,t2,…,tn)，如果si=ti，那么就说对agenti，s和t是不能分辨的（indistinguishable）[11]，并记作s～it，令Ri={(s,t)
8、sÎS,tÎS,s～it}(i=1,2,…,n)，显然Ri(i=1,2,…,n)是与智能体agenti有关的S上的等价关系。因此Kripke结构M可扩充为（S,
