Patent ID: 7146301
Filing Date: 2006-12-05
Classification: G06F

Abstract:
1. A method for checking a model, which defines states of a system under study and a transition relation among the states, the method comprising: specifying a property that applies to a target set that comprises at least one target state among the states of the system under study; beginning from an initial set of at least one initial state among the states of the system, computing successive reachable sets comprising the states of the system that are reachable from the initial set; finding an intersection between one of the reachable sets and the target set; computing a plurality of mutually-disjoint traces from the at least one target state in the intersection through the states in the reachable sets to the at least one initial state, wherein the plurality of mutually-disjoint traces comprises at least one initial trace and at least one subsequently-computed trace; selecting the states on each subsequently-computed trace so as to maximize a distance of the subsequently-computed trace from at least the at least one initial trace; and using the computed traces for checking the model.