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

摘要

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