This book develops the theory of stochastic relations as a foundation for
Markov transition systems. Central topics such as congruences and morphisms
are investigated and applied to the monoidal structure. Bisimilarity
and behavioral equivalence are defined and investigated within this framework;
developments from the general theory of coalgebras are viewed from
the context provided by the subprobability functor. It is shown with these
tools that bisimilarity, behavioral and logical equivalence are the same for general
modal logics and for continuous time stochastic logic with and without
fixed point operator.