a method for checking a model , which defines states of a system under study and a transition relation among the states . the method includes 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 , successive reachable sets are computed , including the states of the system that are reachable from the initial set , until an intersection is found between one of the reachable sets and the target set . a plurality of mutually - disjoint traces are then computed from the at least one target state in the intersection through the states in the reachable sets to the at least one initial state .