Abstract

Dioid based model refinement is an abstract framework for optimality problems on labelled graphs such as the shortest path problem or the maximum capacity problem. Here we show two facts in this area: first, via a language theoretic approach that models with a binary set of edge labels are refinable, and second, the compatibility of linear fixpoint equations with bisimulations. These equations can be used in an algebraic setting for a certain class of optimality problems. Since bisimulations can simplify the complexity of models, they can also reduce the complexity of certain optimality problems.