M.D. Lee and E.P. de Vink
Logical Characterization of Bisimulation for Transition Relations over 
Probability Distributions with Internal Actions

In recent years the study of probabilistic transition systems has shifted to
transition relations over distributions to allow for a smooth adaptation of the
standard non-probabilistic apparatus. In this paper we study transition
relations over probability distributions in a setting with internal actions. We
provide new logics that characterize probabilistic strong, weak and branching
bisimulation. Because these semantics may be considered too strong in the
probabilistic context, Eisentraut et al. recently proposed weak distribution
bisimulation. To show the flexibility of our approach based on the framework of
van Glabbeek for the non-deterministic setting, we provide a novel logical
characterization for the latter probabilistic equivalence as well.