Quantales, finite observations and strong bisimulation

It has often been claimed that bisimulation makes distinctions that cannot be observed in practice. Abramsky and Vickers proposed an algebraic framewo rk based on quantales for describing observations on concurrent processes w ithout hidden transitions and used it in order to provide an "observational explanation" of several process equivalences, ranging from Hoare trace equ ivalence to ready-simulation. We follow their approach and argue that (stro ng) bisimulation can be explained in the same way, at least in the case of "image-computable" labelled transition systems. (C) 2001 Elsevier Science B .V. All rights reserved.