Strong Preservation: An abstraction is strongly preserving when a set of properties with truth values of either true or false in the abstract system consists corresponding properties in the concrete system with the same truth values. Strong preservation may not seem to allow much room for simplifying the system during abstraction. However, because property preservation is defined with respect to a specific property (or a specific class of properties, as in LTL), there are many useful strongly preserving abstractions. Weakly preserving abstractions can be much more aggressive in reducing the state space of a program and therefore they enable more efficient verification. The price paid is that the reported property violations may not correspond to real violations in the concrete, unabstracted program.