关键词: 模型检测, 抽象精化, 虚假反例, 失效状态, 抽象技术

Abstract: In model checking, abstract technology is an effective method to solve the state space explosion, but one of the major obstacles is the abstraction of original system may incur some behaviors that does not exist in the original system, i.e. may incur false counterexamples. Therefore, abstraction refinement should be done based on counterexample. How to judge a counterexample is true or false is very important in the process of abstraction refinement. According to the definition of failure state which is based on pre and post state, the definition of the false counterexample is proposed, and then two algorithms of false counterexample detection are given.

Key words:  , model checking； abstraction refinement； false counterexample； failure state； abstraction technology