概率时态认知逻辑模型检测中三值抽象技术的研究  

Three-Valued Abstraction for Model Checking the Probabilistic Temporal Logic of Knowledge

作　　者：周从华[1,2] 孙博[1,2] 刘志锋[1,2] 葛云[1,2] 

机构地区：[1]江苏大学计算机科学与通信工程学院,镇江212013 [2]南京大学电子科学与工程学院,南京210093

出　　处：《电子学报》2012年第10期2052-2061,共10页Acta Electronica Sinica

基　　金：国家自然科学基金(No.61003288;No.6111130184);江苏省自然科学基金(No.BK2010192);教育部博士点基金(No.20093227110005)

摘　　要：为缓解概率时态认知逻辑模型检测中的状态空间爆炸问题,提出了概率时态认知逻辑的三值抽象技术.具体研究内容包括:定义抽象模型及模型上概率时态认知逻辑的三值语义,依据状态空间等价划分建立初始抽象模型,并证明抽象技术对概率时态认知逻辑的满足性保持关系;提出概率时态认知逻辑模型检测算法;依据初始模型检测的结果,给出利用最小证据和最小反例引导的抽象系统的求精过程.最后通过Dining Cryptographer协议说明了抽象技术的应用,及其在约简系统状态空间方面的效果.In order to overcome the state explosion problem in model checking the probabilisfic temporal logic of knowl edge, a three-valued abstraction is proposed. Our work includes three parts： first the three-value semantics of the probabilistic tempo ral logic of knowledge is defined on the abstract model,and the initial abstract model is build according to the equivalence partition of state space,and the preservation of satisfaction under the abstraction is proved;second the model checking algorithm of the proba- bilistic temporal logic of knowledge is proposed;third how to refine the abslraction by the minimal wimesses and counterexamples generated in model checking is shown. Finally, the abstraction is applied in model checking the Dining Cryptographer protocols.

关 键 词：三值抽象 模型检测 概率时态认知逻辑 反例 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]