In directed model checking, the traversal of the state space is guided by an estimate of the distance from the current state
to the nearest error state. This paper presents a
distance-preserving abstraction for concurrent systems that allows one to compute an interesting estimate of the error distance without hitting the state
explosion problem. Our experiments show a dramatic reduction both in the number of states explored by the model checker and
in the total runtime.