Weak Probabilistic Bisimulation - Semantics of Probabilistic Processes: An Operational Approach - page 241

7.5 Bibliographic Notes

We have considered a notion of weak bisimilarity, which is induced from simulation
preorder. It turns out that this provides both a sound and a complete proof methodol-
ogy for an extensional behavioural equivalence that is a probabilistic version of of the
well-known reduction barbed congruence. This result is extracted from [ 1 ] where
the proofs are carried out for a more general model called Markov automata [ 2 ],
which describe systems in terms of events that may be nondeterministic, may occur
probabilistically, or may be subject to time delays. As a distinguishing feature, the
weak bisimilarity is based on distributions. It is strictly coarser than the state-based
bisimilarity investigated in Sect. 3.5, even in the absence of invisible actions [ 3 ]. A
decision algorithm for the weak bisimilarity is presented in [ 4 ]. For a state-based
weak bisimilarity, a decision algorithm is given in [ 5 ]. Note that by taking the sym-
metric form of Definition 6.19 we can obtain a notion of weak failure bisimulation.
Its characteristics are yet to be explored.
The idea of using barbs as simple experiments [ 6 ] and then deriving reduction
barbed congruence originated in [ 7 ] but has now been widely used for different pro-
cess description languages; for example see [ 8 , 9 ] for its application to higher-order
process languages, [ 10 ] for mobile ambients and [ 11 ] for asynchronous languages.
Incidentally, there are also minor variations on the formulation of reduction barbed
congruence, often called contextual equivalence or barbed congruence , in the
literature. See [ 11 , 12 ] for a discussion of the differences.

References

1. Deng, Y., Hennessy, M.: On the semantics of Markov automata. Inf. Comput. 222 , 139-168
(2013)
2. Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. Pro-
ceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, pp. 342-351.
IEEE Computer Society (2010)
3. Hennessy, M.: Exploring probabilistic bisimulations, part I. Form. Asp. Comput. 24 (4-6),
749-768 (2012)
4. Eisentraut, C., Hermanns, H., Krämer, J., Turrini, A., Zhang, L.: Deciding bisimilarities on
Distributions. Proceedings of the 10th International Conference on Quantitative Evaluation of
Systems, Lecture Notes in Computer Science, vol. 8054, pp. 72-88. Springer (2013)
5. Cattani, S., Segala, R.: Decision Algorithms for Probabilistic Bisimulation. Proceedings of the
13th International Conference on Concurrency Theory, Lecture Notes in Computer Science,
vol. 2421, pp. 371-385. Springer (2002)
6. Rathke, J., Sobocinski, P.: Making the unobservable, unobservable. Electron. Notes Comput.
Sci. 229 (3), 131-144 (2009)
7. Honda, K., Yoshida, N.: On reduction-based process semantics. Theoret. Comput. Sci. 151 (2),
437-486 (1995)
8. Jeffrey, A., Rathke, J.: Contextual equivalence for higher-order pi-calculus revisited. Log.
Methods Comput. Sci. 1 (1:4) (2005)
9. Sangiorgi, D., Kobayashi, N., Sumii, E.: Environmental bisimulations for higher-order lan-
guages. Proceedings of the 22nd IEEE Symposium on Logic in Computer Science, pp. 293-302.
IEEE Computer Society (2007)