Cleaveland R, Iyer P, Yankelevich D.  1995.  Optimality in abstractions of model checking. Static Analysis. :51-63.