Chinese Journal of Computers   Full Text
Title	Model Checking CTL Based on Complete Abstraction Interpretation
Authors	QIAN Jun-Yan1) XU Bao-Wen 2),3)
Address	1) (School of Computer and Control, Guilin University of Electronic Technology, Guilin, Guangxi 541004) 2)(State Key Laboratory for Novel Software Technology, Nanjing University, Nanjing 210093) 3) (Department of Computer Science and Technology, Nanjing University, Nanjing 210093)
Year	2009
Issue	No.5(992—1001)
Abstract &   Background	Abstract Abstraction plays a fundamental role in combating state-space explosion in model checking. In a complete abstract interpretation-based view, the authors 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. The authors show that the abstract domain is complete for the standard operators of CTL iff it is complete for complement and standard predecessor transformer operators. Keywords abstract interpretation; abstract model checking; strong preservation; completeness; refinement Background Model checking is an automatic formal verification technique for a finite state system, where all the states of the system are exhaustively enumerated and the correctness condition checked at each state, and also yields extremely useful counter examples if model checking fails. As key issue in model checking, abstraction is a method for reducing the state space of the checked system. When model checking using abstraction, the main concern is that the abstractions must be property-preserving. There are two forms of property preservation: Weak Preservation and Strong Preservation. Strong preservation is related to completeness in abstract interpretation by studying the relationship between complete abstract interpretations, strongly preserving and spurious counterexamples of abstract model checking. In order to eliminate spurious counterexamples, a method is designed for minimally making abstract interpretations complete. It is showed that completeness of an abstract interpretation is a property which does not depend on the abstract semantic operations but on the underlying abstract domains only. This opened up the question of making abstract interpretations complete by least refinements of abstract domains. However, this least refinement always exists and can be constructively characterized as fixed point solution of abstract domain equations. This work is supported by the National Natural Science Foundations for Distinguished Young Scholar under grant No.60425206, the National Natural Science Foundation of China under grant Nos.90818027, 60633010, 60663005 and the National High Technology Research and Development Program (863 Program) of China under grant No.2009AA01Z147.