Time-memory tradeoff control in counterexample production

Apparatus for checking a model, which defines states of a system under study and a transition relation among the states, the apparatus comprising:

• a memory, adapted to store data;
• and
• a model processor, which is arranged to receive a property that applies to a target set that comprises one or more target states among the states of the system under study, and to compute, beginning with an initial set of one or more initial states among the states of the system, 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, such that while computing the sets, the processor selects one or more of the sets in the succession to be saved in the memory, while the sets not selected are discarded, the processor being further arranged to find an intersection between one of the sets in the succession and the target set, and to compute 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.

A computer software product for checking a model, which defines states of a system under study and a transition relation among the states, the product comprising a computer-readable medium in which program instructions are stored, which instructions, when read by a computer, cause the computer to receive a property that applies to a target set that comprises one or more target states among the states of the system under study, and to compute, beginning with an initial set of one or more initial states among the states of the system, 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, such that while computing the sets, the computer selects one or more of the sets in the succession to be saved in the memory, while the sets not selected are discarded, the instructions further causing the computer to find an intersection between one of the sets in the succession and the target set, and to compute 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.