东篱科研大数据发现系统（DRDS）

位置：成果数据库 > 期刊 > 期刊详情页

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

ISSN号：0732-2112
期刊名称：电子学报
时间：2012.10.10
页码：2052-2061
分类：TP301[自动化与计算机技术—计算机系统结构;自动化与计算机技术—计算机科学与技术]
作者机构：[1]江苏大学计算机科学与通信工程学院,镇江212013, [2]南京大学电子科学与工程学院,南京210093
相关基金：国家自然科学基金（№.61003288,No.6111130184）;江苏省自然科学基金（No.BK2010192）;教育部博士点基金（No.20093227110005）
相关项目：信息流安全属性算术验证的研究

关键词：三值抽象, 模型检测, 概率时态认知逻辑, 反例, three-valued abstraction, model checking, probabilistic temporal logic of knowledge, counterexample

中文摘要：

为缓解概率时态认知逻辑模型检测中的状态空间爆炸问题，提出了概率时态认知逻辑的三值抽象技术．具体研究内容包括：定义抽象模型及模型上概率时态认知逻辑的三值语义，依据状态空间等价划分建立初始抽象模型，并证明抽象技术对概率时态认知逻辑的满足性保持关系；提出概率时态认知逻辑模型检测算法；依据初始模型检测的结果，给出利用最小证据和最小反例引导的抽象系统的求精过程．最后通过DiningCryptographer协议说明了抽象技术的应用，及其在约简系统状态空间方面的效果．

英文摘要：

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.

同期刊论文项目