Taking chances on MERGE and FAIL: Extending strong and probabilistic bisimulation

For a process language, featuring nondeterministic and probabilistic choice, a parallel operator and a failure construct, a notion of bisimulation is proposed. As one can interpret recovery from failure with respect to nondeterministic and probabilistic choice in various ways, a single transition system gives rise to several operational models. A uniform way to abstract the `first steps' underlies, for each of these models, the definition of the proposed bisimulation. This bisimulation specializes to Park-Milner bisimulation for the non-probabilistic fragment of the language on the one hand, and to Larsen-Skou bisimulation for the deterministic/probabilistic part of the language, on the other hand. Furthermore, a conditional congruence result is obtained