A Definition Scheme for Quantitative Bisimulation
Diego Latella, Mieke Massink and Erik de Vink

FuTS, state-to-function transition systems are generalizations of
labeled transition systems and of familiar notions of quantitative
semantical models as continuous-time Markov chains, interactive Markov
chains, and Markov automata. A general scheme for the definition of a
notion of strong bisimulation associated with a FuTS is proposed. It
is shown that this notion of bisimulation for a FuTS coincides with
the coalgebraic notion of behavioral equivalence associated to the
functor on Set given by the type of the FuTS. For a series of concrete
quantitative semantical models the notion of bisimulation as reported
in the literature is proven to coincide with the notion of
quantitative bisimulation obtained from the scheme. The comparison
includes models with orthogonal behaviour, like interactive Markov
chains, and with multiple levels of behavior, like Markov automata. As
a consequence of the general result relating FuTS bisimulation and
behavioral equivalence we obtain, in a systematic way, a coalgebraic
underpinning of all quantitative bisimulations discussed.