the abstraction in order to remove the artificial computations that may appear in the approximate analysis by considering how the concrete system behaves when false alarms or spurious traces are encountered. The general concept of using spurious counterexamples for refining an abstraction stems from the CounterExample-Guided Abstraction Refinement (CEGAR) paradigm [@cgjlv00; @cgjlv03]. The model here drives the automatic identification of prefixes of the counterexample path that do not correspond to an actual trace in the concrete model, by isolating abstract (failure) states that need to be refined in order to eliminate that spurious counterexample. Model-driven refinements, such as CEGAR, provide algorithmic methods for achieving abstractions that are complete (i.e., precise [@gq01; @grs00]) with respect to some given property of the concrete model.

We investigate here the dual problem of *abstraction simplification*. Instead of refining abstractions in order to eliminate spurious traces, our goal is to simplify an abstraction $A$ towards a simpler (ideally, the simplest) model $A_s$ that maintains the same approximate behavior as $A$ does. In abstract model checking, this abstraction simplification has *to keep the same examples* of the concrete system in the following sense. Recall that an abstract path $\pi$ in an abstract transition system ${\mathcal{A}}$ is 