Abstract
A known generic strategy for handling large transition systems is the combined use of bisimulations and refinement. The idea is to reduce a large system by means of a bisimulation quotient into a smaller one, then to refine the smaller one in such way that it fulfils a desired property, and then to expand this refined system back into a submodel of the original one. This generic algorithm is not guaranteed to work correctly for every desired property; here we show its correctness for a class of optimality problems which can be described in the framework of dioids.