I will discuss a notion of equivalence between two probabilistic systems introduced by Larsen and Skou in 89 called probabilistic bisimulation.

In particular, I will look at logical characterizations for this notion: the goal is to describe a logic such that two systems are bisimilar if and only if they satisfy the same formulas. This question goes all the way back to Hennessey and Millner for non probabilistic transition systems.

I will develop topological tools and give very general logical characterization results for probabilistic simulation and bisimulation.