In a category of labeled transition systems with `path-lifting' morphisms the largest self-bisimulation on an object determines a a quotient which provides a compositional minimization theory described by a lax monad. An application to model checking is discussed. A behaviour taking values in certain trees allows an adjoint minimal realization theory.
This is joint work with P. Katis, N. Sabadini, and R. Walters