Patent Document ID: 20020178423
Application ID: 10042293
Patent Status: 0

Claim One:
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 one or more target states among the states of the system under study; beginning with an initial set of one or more initial states among the states of the system, computing a succession of sets of the states of the system, such that the states in each of the sets are reachable by a successive cycle of the transition relation from the states in a preceding set in the succession; selecting one or more of the sets in the succession to be saved in a memory, while the sets not selected are discarded; finding an intersection between one of the sets in the succession and the target set; and computing a trace from one of the target states in the intersection through the states in the sets in the succession, including the discarded sets, to one of the initial states, using the sets saved in the memory to reconstruct the discarded sets.