Completeness of bounded model checking temporal logic of knowledge  

知识时态逻辑有界模型检测中的完备性(英文)

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

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

出　　处：《Journal of Southeast University(English Edition)》2010年第3期399-405,共7页东南大学学报（英文版）

基　　金：The National Natural Science Foundation of China (No.10974093);the Scientific Research Foundation for Senior Personnel of Jiangsu University (No.07JDG014);the Natural Science Foundation of Higher Education Institutions of Jiangsu Province (No.08KJD520015)

摘　　要：In order to find the completeness threshold which offers a practical method of making bounded model checking complete, the over-approximation for the complete threshold is presented. First, a linear logic of knowledge is introduced into the past tense operator, and then a new temporal epistemic logic LTLKP is obtained, so that LTLKP can naturally and precisely describe the system＇s reliability. Secondly, a set of prior algorithms are designed to calculate the maximal reachable depth and the length of the longest of loop free paths in the structure based on the graph structure theory. Finally, some theorems are proposed to show how to approximate the complete threshold with the diameter and recurrence diameter. The proposed work resolves the completeness threshold problem so that the completeness of bounded model checking can be guaranteed.为解决限界模型检测的完备性问题,研究了完全界的计算问题,给出了完全界的上近似计算.首先,在线性时态认知逻辑中引入过去时态算子,得到新的时态认知逻辑LTLPK,从而可以紧凑自然地描述系统的可靠性规范;其次,依据图结构理论,设计了一套深度优先算法计算出系统的最大可达深度和最长无循环路径的长度;最后,以定理的形式给出了最大可达深度和最长无循环路径的长度与完全界的关系,得出了完全界的一种上近似估算.所做工作有效地解决了限界模型检测中的完全界计算问题,从而保证了限界模型检测的完备性.

关 键 词：bounded model checking temporal logics of knowledge multi-agent system 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]