An algebraic characterization of observational equivalence

We show that observational equivalence can be characterized by saturating homomorphisms (with respect to Hennessy-Milner logic), thus bringing together results developed independently by Castellani and by Arnold and Dicky on characterizations of transition system equivalences. We take this opportunity to compare Castellani's abstraction homomorphisms and Arnold-Dicky's saturating homomorphisms. It turns out that they are very similar notions: their difference in formulation is partly due to the fact that abstraction homomorphisms were defined on a restricted class of transition systems.