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

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

为缓解概率时态认知逻辑模型检测中的状态空间爆炸问题,提出了概率时态认知逻辑的三值抽象技术.具体研究内容包括:定义抽象模型及模型上概率时态认知逻辑的三值语义,依据状态空间等价划分建立初始抽象模型,并证明抽象技术对概率时态认知逻辑的满足性保持关系;提出概率时态认知逻辑模型检测算法;依据初始模型检测的结果,给出利用最小证据和最小反例引导的抽象系统的求精过程.最后通过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.