Patent ID: 8627273

Claim:
A computerized system comprising: a processor; an interface for receiving a phase abstracted model, the phase abstracted model is a result of a phase abstraction transformation on an original model having an original transition relation, wherein a transition relation of the phase abstracted model represents a plurality of transitions using the original transition relation; an interface for receiving an original liveness specification property that is to be held by the original model; a property modifier for transforming the original liveness specification property to a phase abstracted liveness specification property in accordance with the phase abstraction transformation, wherein the transformation is based on the phase abstracted model, wherein a falsification by the phase abstracted model of the phase abstracted liveness specification property corresponds to a falsification by the original model of the original liveness specification property; and a counter-example manipulation module for transforming an original counter-example to a modified counter-example, the original counter-example exemplifies a falsification of the phase abstracted liveness specification property in respect to the phase abstracted model, the modified counter-example exemplifies a falsification of the original liveness specification property in respect to the original model.