概率时态认知逻辑模型检测中三值抽象技术的研究
周从华;孙博;刘志锋;葛云
【期刊名称】《电子学报》 【年(卷),期】2012(040)010
【摘要】In order to overcome the state explosion problem in model checking the probabilistic temporal logic of knowledge, a three-valued abstraction is proposed. Our work includes three parts: first the three-value semantics of the probabilistic temporal 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 probabilistic temporal logic of knowledge is proposed; third how to refine the abstraction by the minimal witnesses and counterexamples generated in model checking is shown.Finally,the abstraction is applied in model checking the Dining Cryptographer protocols.%为缓解概率时态认知逻辑模型检测中的状态空间爆炸问题,提出了概率时态认知逻辑的三值抽象技术.具体研究内容包括:定义抽象模型及模型上概率时态认知逻辑的三值语义,依据状态空间等价划分建立初始抽象模型,并证明抽象技术对概率时态认知逻辑的满足性保持关系；提出概率时态认知逻辑模型检测算法；依据初始模型检测的结果,给出利用最小证据和最小反例引导的抽象系统的求精过程.最后通过Dining Cryptographer协议说明了抽象技术的应用,及其在约简系统状态空间方面的效果.
【总页数】10页(2052-2061)
【关键词】三值抽象;模型检测;概率时态认知逻辑;反例 【作者】周从华;孙博;刘志锋;葛云
【作者单位】江苏大学计算机科学与通信工程学院,镇江,212013;南京大学电子科学与工程学院,南京,210093;; 【正文语种】中文 【中图分类】TP301 【文献来源】
https://www.zhangqiaokeyan.com/academic-journal-cn_acta-electronica-sinica_thesis/0201233740573.html 【相关文献】
1.概率实时时态认知逻辑模型检测中抽象技术的研究 [J], 刘志锋; 孙博; 周从华 2.有界模型检测同步多智体系统的时态认知逻辑 [J], 骆翔宇; 苏开乐; 杨晋吉 3.基于时态认知逻辑的Web服务模型检测 [J], 骆翔宇; 陈艳; 古天龙; 董荣胜 4.智能主体的信念认知时态子结构逻辑模型 [J], 刘冬宁; 汤庸 5.时态认知逻辑CTL*K的符号化模型检查算法 [J], 陈彬; 王智学
以上内容为文献基本信息，获取文献全文请下载
概率时态认知逻辑模型检测中三值抽象技术的研究
