Using Bisimulations for Optimality Problems in Model Refinement

erschienen 2011 in H. de Swart (eds.): Relational and Algebraic Methods in Computer Science (RAMiCS 12), LNCS 6663, 2011.

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.