基于完备抽象解释的模型检验CTL公式研究.doc

基于完备抽象解释的模型检验CTL公式研究* 钱俊彦1) 徐宝文2),3) 1)(桂林电子科技大学 计算机与控制学院, 广西 桂林 541004) 2)(南京大学 计算机软件新技术国家重点实验室, 江苏 南京 210093) 3)(南京大学 计算机科学与技术系, 江苏 南京 210093) 摘 要: 在模型检验中，抽象是解决状态空间爆炸问题的重要方法之一。给定具体Kripke结构和时序描述语言CTL，基于抽象解释框架，以及完备抽象解释和性质强保留之间的关系，抽象模型最小精化使得CTL性质强保留，可转换为抽象解释中抽象域的最小完备精化，并且总是存在抽象域的最小完备精化。根据状态标签函数确定初始抽象域，然后通过不动点求解，获得对CTL标准算子完备的最小抽象域，并依据此抽象域求得CTL性质强保留的最优抽象状态划分，最后构造出CTL性质强保留且最优的抽象状态转换系统。并出抽象域对CTL标准算子是完备的当且仅当抽象域对补集和标准前向转换是完备的。 1), XU Bao-wen 2),3) 1) (Department of Computer and Control, Guilin University of Electronic Technology, Guilin 541004, China) 2) (State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing 210093, China) 3) (Department of Computer Science and Technology, Nanjing University, Nanjing 210093, China) Abstract. Abstraction plays a fundamental role in combating state-space explosion in model checking. In a complete abstract interpretation-based view, we reduce the state space of a Kripke structure in order to obtain a minimal abstract state translation system that strongly preserves a given temporal specification language CTL. According to a relation between completeness of abstract interpretations and strong preservation of abstract model checking, the problem of minimally refining abstract model in order to make it strongly preserving CTL can be formulated as a minimal abstract domain refinement in abstraction interpretation in order to get completeness, and this refined complete abstract domain always exists. Given initial abstract domain, we can obtain a minimal abstract domain which is complete for the standard operators of CTL by the iterative computation of the fixpoint. Moreover, the corresponding partition is the coarsest partition which is strong preserving for CTL. We show that the abstract domain is complete for the standard operators of CTL iff it is complete for complement and standard predecessor transformer operators. Key words: Abstract interpretation, abstract model checking, strong preservation, completeness, ref