中文摘要：

为解决限界模型检测的完备性问题,研究了完全界的计算问题,给出了完全界的上近似计算.首先,在线性时态认知逻辑中引入过去时态算子,得到新的时态认知逻辑LTLPK,从而可以紧凑自然地描述系统的可靠性规范;其次,依据图结构理论,设计了一套深度优先算法计算出系统的最大可达深度和最长无循环路径的长度;最后,以定理的形式给出了最大可达深度和最长无循环路径的长度与完全界的关系,得出了完全界的一种上近似估算.所做工作有效地解决了限界模型检测中的完全界计算问题,从而保证了限界模型检测的完备性.

英文摘要：

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.