SEARCHING FOR COUNTER-EXAMPLES INTELLIGENTLY

摘要

A method for finding a counterexample on a system of states, including one or more initial states and one or more bad states, and a transition relation among the states. The method includes assembling a first set of the states known to be reachable from the initial states in accordance with the transition relation, and defining a second set of the states from which it is estimated that one of the bad states is reachable in accordance with the transition relation. The sets of the states are modified until a definition of the second set is found such that from one or more of the states in an intersection of the first and second sets, there is at least one of the bad states that can be reached in a given number of steps of the transition relation. The counterexample is searched for over the states in the intersection.