  Several notions of bisimulation relations for probabilistic non-deterministic
transition systems have been considered in the literature. We consider a novel
testing-based behavioral equivalence called upper-expectation bisimilarity and
develop its theory using standard results from linear algebra and functional
analysis. We show that, for a wide class of systems, our new notion coincides
with Segala's convex bisimilarity. We develop logical characterizations in
terms of expressive probabilistic modal mu-calculi and a novel real-valued
modal logic. We prove that upper-expectation bisimilarity is a congruence for
the wide family of process algebras specified following the probabilistic GSOS
rule format.
