Probabilistic bisimulation

Probabilistic bisimulation is an extension of the concept of bisimulation for fully probabilistic transition systems.A discrete probabilistic transition system is a triple

$S\; =\; (St,Act,\; au:St\; imes\; Act\; imes\; St\; ightarrow\; [0,1]\; )$

where $au(s,a,t)$ gives the probability of starting in the state s, performing the action a and endingup in the state t. The set of states is assumed to be countable. There is no attempt to assign probabilities to actions. It is assumed that the actions are chosen nondeterministically by an adversary or by the environment. This type of system is fully probabilistic, there is no other indeterminacy.

The definition of a probabilistic bisimulation on a system S is an equivalence relation R on the state space St, such that forevery pair s,t in St with sRt and for every action a in Act and for every equivalence class C of R$au(s,a,C)\; =\; au(t,a,C).$Two states are said to be probabilistically bisimilar if there is some such R relating them.

ources

*The definition is due to K. G. Larsen and A. Skou and appeared in the article "Bisimulation through Probablistic Testing", published in Information and Computation, vol 94, pages 1-28, 1991.