Skip to main content
SpringerLink
Log in

Probabilistic Bisimulation

  • Chapter
  • First Online:
Semantics of Probabilistic Processes

  • 513 Accesses

Abstract

We introduce the operational model of probabilistic labelled transition systems, where a state evolves into a distribution after performing some action. To define relations between distributions, we need to lift a relation on states to be a relation on distributions of states. There is a natural lifting operation that nicely corresponds to the Kantorovich metric, a fundamental concept used in mathematics to lift a metric on states to a metric on distributions of states, which is also related to the maximum flow problem in optimisation theory.

The lifting operation yields a neat notion of probabilistic bisimulation, for which we provide logical, metric and algorithmic characterisations. Specifically, we extend the Hennessy–Milner logic and the modal mu-calculus with a new modality, resulting in an adequate and an expressive logic for probabilistic bisimilarity. The correspondence of the lifting operation and the Kantorovich metric lead to a characterisation of bisimulations as pseudometrics that are postfixed points of a monotone function. Probabilistic bisimilarity also admits both partition refinement and “on-the-fly” decision algorithms; the latter exploits the close relationship between the lifting operation and the maximum flow problem.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Hardcover Book
USD 54.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    We use a pseudometric rather than a proper metric because two distinct states can still be at distance zero if they are bisimilar.

  2. 2.

    For simplicity, in this section we use the term metric to denote both metric and pseudometric. All the results are based on pseudometrics.

References

  1. Giacalone, A., Jou, C.C., Smolka, S.A.: Algebraic reasoning for probabilistic concurrent systems. Proceedings of IFIP TC2 Working Conference on Programming Concepts and Methods, Sea of Galilee, Israel (1990)

    Google Scholar 

  2. Christoff, I.: Testing equivalences and fully abstract models for probabilistic processes. Proceedings of the 1st International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 458, pp. 126–140. Springer, Heidelberg (1990)

    Google Scholar 

  3. Larsen, K.G., Skou, A.: Compositional verification of probabilistic processes. Proceedings of the 3rd International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 630, pp. 456–471. Springer, Heidelberg (1992)

    Google Scholar 

  4. Hansson, H., Jonsson, B.: A calculus for communicating systems with time and probabilities. Proceedings of IEEE Real-Time Systems Symposium, pp. 278–287. IEEE Computer Society Press (1990)

    Google Scholar 

  5. Yi, W., Larsen, K.G.: Testing probabilistic and nondeterministic processes. Proceedings of the IFIP TC6/WG6.1 12th International Symposium on Protocol Specification, Testing and Verification, IFIP Transactions, vol. C-8, pp. 47–61. North-Holland (1992)

    Google Scholar 

  6. Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. Proceedings of the 5th International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 836, pp. 481–496. Springer, Heidelberg (1994)

    Google Scholar 

  7. Lowe, G.: Probabilistic and prioritized models of timed CSP. Theor. Comput. Sci. 138, 315–352 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  8. Segala, R.: Modeling and verification of randomized distributed real-time systems. Tech. Rep. MIT/LCS/TR-676, PhD thesis, MIT, Dept. of EECS (1995)

    Google Scholar 

  9. Morgan, C.C., McIver, A.K., Seidel, K.: Probabilistic predicate transformers. ACM Trans. Progr. Lang. Syst. 18(3), 325–353 (1996)

    Article  Google Scholar 

  10. He, J., Seidel, K., McIver, A.K.: Probabilistic models for the guarded command language. Sci. Comput. Program. 28, 171–192 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  11. Huth, M., Kwiatkowska, M.: Quantitative analysis and model checking. Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, pp. 111–122. IEEE Computer Society (1997)

    Google Scholar 

  12. McIver, A., Morgan, C.: An expectation-based model for probabilistic temporal logic. Tech. Rep. PRG-TR-13-97, Oxford University Computing Laboratory (1997)

    Google Scholar 

  13. Bandini, E., Segala, R.: Axiomatizations for probabilistic bisimulation. Proceedings of the 28th International Colloquium on Automata, Languages and Programming, Lecture Notes in Computer Science, vol. 2076, pp. 370–381. Springer (2001)

    Google Scholar 

  14. Jonsson, B., Yi, W.: Testing preorders for probabilistic processes can be characterized by simulations. Theor. Comput. Sci. 282(1), 33–51 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  15. Mislove, M.M., Ouaknine, J., Worrell, J.: Axioms for probability and nondeterminism. Electron. Notes Theor. Comput. Sci. 96, 7–28 (2004)

    Article  Google Scholar 

  16. Cleaveland, R., Iyer, S.P., Narasimha, M.: Probabilistic temporal logics via the modal mucalculus. Theor. Comput. Sci. 342(2–3), 316–350 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  17. Tix, R., Keimel, K., Plotkin, G.: Semantic domains for combining probability and non-determinism. Electron. Notes Theor. Comput. Sci. 129, 1–104 (2005)

    Article  MathSciNet  Google Scholar 

  18. McIver, A., Morgan, C.: Results on the quantitative mu-calculus. ACM Trans. Comput. Logic 8(1) (2007)

    Google Scholar 

  19. Deng, Y., van Glabbeek, R., Hennessy, M., Morgan, C.C., Zhang, C.: Remarks on testing probabilistic processes. Electron Notes Theor. Comput. Sci. 172, 359–397 (2007)

    Article  MathSciNet  Google Scholar 

  20. Deng, Y., van Glabbeek, R., Morgan, C.C., Zhang, C.: Scalar outcomes suffice for finitary probabilistic testing. Proceedings of the 16th European Symposium on Programming. Lecture Notes in Computer Science, vol. 4421, pp. 363–378. Springer, Heidelberg (2007)

    Google Scholar 

  21. Deng, Y., van Glabbeek, R., Hennessy, M., Morgan, C.C.: Characterising testing preorders for finite probabilistic processes. Log. Methods Comput. Sci. 4(4), 1–33(2008)

    Article  MathSciNet  Google Scholar 

  22. Deng, Y., van Glabbeek, R., Hennessy, M., Morgan, C.: Testing finitary probabilistic processes (extended abstract). Proceedings of the 20th International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 5710, pp. 274–288. Springer, Heidelberg (2009)

    Google Scholar 

  23. Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1–28 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  24. Deng, Y., Du, W.: Probabilistic barbed congruence. Electron. Notes Theor. Comput. Sci. 190(3), 185–203 (2007)

    Article  Google Scholar 

  25. Kantorovich, L.: On the transfer of masses (in Russian). Dokl. Akademii Nauk 37(2), 227–229 (1942)

    Google Scholar 

  26. Baier, C., Engelen, B., Majster-Cederbaum, M.E.: Deciding bisimilarity and similarity for probabilistic processes. J. Comput. Syst. Sci. 60(1), 187–231 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  27. Milner, R.: Communication and Concurrency. Prentice Hall, Upper Saddle River (1989)

    Google Scholar 

  28. Park, D.: Concurrency and automata on infinite sequences. Proceedings of the 5th GI-Conference on Theoretical Computer Science. Lecture Notes in Computer Science, vol. 104, pp. 167–183. Springer, Heidelberg (1981)

    Google Scholar 

  29. Pnueli, A.: Linear and branching structures in the semantics and logics of reactive systems. Proceedings of the 12th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 194, pp. 15–32. Springer, Heidelberg (1985)

    Google Scholar 

  30. Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. the ACM 32(1), 137–161 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  31. Kozen, D.: Results on the propositional mu-calculus. Theor. Comput. Sci. 27, 333–354 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  32. Monge, G.: Mémoire sur la théorie des déblais et des remblais. Histoire de l’Academie des Science de Paris p. 666 (1781)

    Google Scholar 

  33. Vershik, A.: Kantorovich metric: Initial history and little-known applications. J. Math. Sci. 133(4), 1410–1417 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  34. Orlin, J.B.: A faster strongly polynomial minimum cost flow algorithm. Proceedings of the 20th ACM Symposium on the Theory of Computing, pp. 377–387. ACM (1988)

    Google Scholar 

  35. Deng, Y., Du, W.: Kantorovich metric in computer science: A brief survey. Electron. Notes Theor. Comput. Sci. 353(3), 73–82 (2009)

    Article  Google Scholar 

  36. Gibbs, A.L., Su, F.E.: On choosing and bounding probability metrics. Int. Stat. Rev. 70(3), 419–435 (2002)

    Article  MATH  Google Scholar 

  37. Rachev, S.: Probability Metrics and the Stability of Stochastic Models. Wiley, New York (1991)

    MATH  Google Scholar 

  38. Kantorovich, L.V., Rubinshtein, G.S.: On a space of totally additive functions. Vestn Len. Univ. 13(7), 52–59 (1958)

    MATH  Google Scholar 

  39. Villani, C.: Topics in Optimal Transportation, Graduate Studies in Mathematics, vol. 58. American Mathematical Society (2003)

    Google Scholar 

  40. van Breugel, F., Worrell, J.: An algorithm for quantitative verification of probabilistic transition systems. Proceedings of the 12th International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 2154, pp. 336–350. Springer, Heidelberg (2001)

    Google Scholar 

  41. Even, S.: Graph Algorithms. Computer Science Press, Potomac (1979)

    Google Scholar 

  42. Ford, L., Fulkerson, D.: Flows in Networks. Princeton University Press, Princeton (2010)

    Google Scholar 

  43. Aharonia, R., Bergerb, E., Georgakopoulosc, A., Perlsteina, A., Sprüssel, P.: The max-flow min-cut theorem for countable networks. J. Comb. Theory, Ser. B 101(1), 1–17 (2011)

    Article  Google Scholar 

  44. Sack, J., Zhang, L.: Ageneral framework for probabilistic characterizing formulae. Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 7148, pp. 396–411. Springer, Heidelberg (2012)

    Google Scholar 

  45. Hermanns, H., Parma, A. et al.: Probabilistic logical characterization. Inf. Comput. 209(2), 154–172 (2011)

    Google Scholar 

  46. Desharnais, J., Edalat, A., Panangaden, P.: A logical characterization of bisimulation for labelled Markov processes. Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science, pp. 478–489. IEEE Computer Society Press (1998)

    Google Scholar 

  47. Parma, A., Segala, R.: Logical characterizations of bisimulations for discrete probabilistic systems. Proceedings of the 10th International Conference on Foundations of Software Science and Computational Structures. Lecture Notes in Computer Science, vol. 4423, pp. 287–301. Springer, Heidelberg (2007)

    Google Scholar 

  48. van Breugel, F., Mislove, M., Ouaknine, J., Worrell, J.: Domain theory, testing and simulation for labelled Markov processes. Theor. Comput. Sci. 333(1–2), 171–197 (2005)

    Article  MATH  Google Scholar 

  49. Sangiorgi, D., Rutten, J. (eds.): Advanced Topics in Bisimulation and Coinduction. Cambridge University Press, NewYork (2011)

    Google Scholar 

  50. Doberkat, E.E.: Stochastic Coalgebraic Logic. Springer, Heidelberg (2010)

    MATH  Google Scholar 

  51. Deng, Y., Wu, H.: Modal Characterisations of Probabilistic and Fuzzy Bisimulations. Proceedings of the 16th International Conference on Formal Engineering Methods. Lecture Notes in Computer Science, vol. 8829, pp. 123–138. Springer, Heidelberg (2014)

    Google Scholar 

  52. Tarski, A.: A lattice-theoretical fixpoint theorem and its application. Pac. J. Math. 5, 285–309 (1955)

    Article  MATH  MathSciNet  Google Scholar 

  53. Steffen, B., Ingólfsdóttir, A.: Characteristic formulae for processes with divergence. Inf. Comput. 110, 149–163 (1994)

    Article  MATH  Google Scholar 

  54. Müller-Olm, M.: Derivation of characteristic formulae. Electron. Notes Theor. Comput. Sci. 18, 159–170 (1998)

    Article  Google Scholar 

  55. van Breugel, F., Worrell, J.: Towards quantitative verification of probabilistic transition systems. Proceedings of the 28th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 2076, pp. 421–432. Springer, Heidelberg (2001)

    Google Scholar 

  56. Desharnais, J., Jagadeesan, R., Gupta, V., Panangaden, P.: The metric analogue of weak bisimulation for probabilistic processes. Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, pp. 413–422. IEEE Computer Society (2002)

    Google Scholar 

  57. Desharnais, J., Jagadeesan, R., Gupta, V., Panangaden, P.: Metrics for labelled markov processes. Theor. Comput. Sci. 318(3), 323–354 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  58. Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  59. Kanellakis, P., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput. 86(1), 43–65 (1990)

    Article  MATH  MathSciNet  Google Scholar 

  60. Cheriyan, J., Hagerup, T., Mehlhorn, K.: Can a maximum flow be computed on O(nm) time? Proceedings of the 17th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 443, pp. 235–248. Springer, Heidelberg (1990)

    Google Scholar 

  61. Lin, H.: “On-the-fly” instantiation of value-passing processes. Proceedings of FORTE'98, IFIP Conference Proceedings, vol. 135, pp. 215–230. Kluwer (1998)

    Google Scholar 

  62. Fernandez, J.C., Mounier, L.: Verifying bisimulations “on the fly”. Proceedings of the 3rd International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, pp. 95–110. North-Holland (1990)

    Google Scholar 

  63. Deng, Y., Du, W.: A local algorithm for checking probabilistic bisimilarity. Proceedings of the 4th International Conference on Frontier of Computer Science and Technology, pp. 401–409. IEEE Computer Society (2009)

    Google Scholar 

  64. Rabin, M.O.: Probabilistic automata. Inf. Control 6, 230–245 (1963)

    Article  MATH  Google Scholar 

  65. Derman, C.: Finite State Markovian Decision Processes. Academic, New York (1970)

    MATH  Google Scholar 

  66. Vardi, M.: Automatic verification of probabilistic concurrent finite-state programs. Proceedings 26th Annual Symposium on Foundations of Computer Science, pp. 327–338 (1985)

    Google Scholar 

  67. Jones, C., Plotkin, G.: A probabilistic powerdomain of evaluations. Proceedings of the 4th Annual IEEE Symposium on Logic in Computer Science, pp. 186–195. Computer Society Press (1989)

    Google Scholar 

  68. van Glabbeek, R., Smolka, S.A., Steffen, B., Tofts, C.: Reactive, generative, and stratified models of probabilistic processes. Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science, pp. 130–141. Computer Society Press (1990)

    Google Scholar 

  69. Jonsson, B., Ho-Stuart, C., Yi, W.: Testing and refinement for nondeterministic and probabilistic processes. Proceedings of the 3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems. Lecture Notes in Computer Science, vol. 863, pp. 418–430. Springer, Heidelberg (1994)

    Google Scholar 

  70. Jonsson, B., Yi, W.: Compositional testing preorders for probabilistic processes. Proceedings of the 10th Annual IEEE Symposium on Logic in Computer Science, pp. 431–441. Computer Society Press (1995)

    Google Scholar 

  71. Puterman, M.L.: Markov Decision Processes. Wiley, New York (1994)

    Book  MATH  Google Scholar 

  72. Crafa, S., Ranzato, F.: Aspectrum of behavioral relations over LTSs on probability distributions. Proceedings the 22nd International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 6901, pp. 124–139. Springer, Heidelberg (2011)

    Google Scholar 

  73. Hennessy, M.: Exploring probabilistic bisimulations, part I. Form. Asp. Comput. 24(4–6), 749–768 (2012)

    Article  MATH  MathSciNet  Google Scholar 

  74. Feng, Y., Zhang, L.: When equivalence and bisimulation join forces in probabilistic automata. Proceedings of the 19th International Symposium on Formal Methods. Lecture Notes in Computer Science, vol. 8442, pp. 247–262. Springer, Heidelberg (2014)

    Google Scholar 

  75. van Glabbeek, R.: The linear time-branching time spectrum I; the semantics of concrete, sequential processes. Handbook of Process Algebra, Chapter 1, pp. 3–99. Elsevier (2001)

    Google Scholar 

  76. van Breugel, F., Worrell, J.: Approximating and computing behavioural distances in probabilistic transition systems. Theor. Comput Sci. 360(1–3), 373–385 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  77. van Breugel, F., Sharma, B., Worrell, J.: Approximating a behavioural pseudometric without discount for probabilistic systems. Proceedings of the 10th International Conference on Foundations of Software Science and Computational Structures. Lecture Notes in Computer Science, vol. 4423, pp. 123–137. Springer, Heidelberg (2007)

    Google Scholar 

  78. van Breugel, F., Worrell, J.: A behavioural pseudometric for probabilistic transition systems. Theor. Comput. Sci. 331(1), 115–142 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  79. van Breugel, F., Hermida, C., Makkai, M., Worrell, J.: An accessible approach to behavioural pseudometrics. Proceedings of the 32nd International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 3580, pp. 1018–1030. Springer, Heidelberg (2005)

    Google Scholar 

  80. van Breugel, F., Hermida, C., Makkai, M., Worrell, J.: Recursively defined metric spaces without contraction. Theor. Comput. Sci. 380(1–2), 143–163 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  81. Desharnais, J., Jagadeesan, R., Gupta, V., Panangaden, P.: Metrics for labeled Markov systems. Proceedings of the 10th International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 1664, pp. 258–273. Springer-Verlag, Heidelberg (1999)

    Google Scholar 

  82. Ferns, N., Panangaden, P., Precup, D.: Metrics for finite Markov decision processes. Proceedings of the 20th Conference in Uncertainty in Artificial Intelligence, pp. 162–169. AUAI Press (2004)

    Google Scholar 

  83. Ferns, N., Panangaden, P., Precup, D.: Metrics for Markov decision processes with infinite state spaces. Proceedings of the 21st Conference in Uncertainty in Artificial Intelligence, pp. 201–208. AUAI Press (2005)

    Google Scholar 

  84. Deng, Y., Chothia, T., Palamidessi, C., Pang, J.: Metrics for action-labelled quantitative transition systems. Electron. Notes Theor. Comput. Sci. 153(2), 79–96 (2006)

    Article  Google Scholar 

  85. Chatzikokolakis, K., Gebler, D., Palamidessi, C., Xu, L.: Generalized bisimulation metrics. Proceedings of the 25th International Conference on Concurrency Theory. Lecture Notes in Computer Science, vol. 8704, pp. 32–46. Springer, Heidelberg (2014)

    Google Scholar 

  86. Ying, M.: Bisimulation indexes and their applications. Theor. Comput. Sci. 275, 1–68 (2002)

    Article  MATH  Google Scholar 

  87. Zhang, L., Hermanns, H., Eisenbrand, F., Jansen, D.N.: Flow faster: Efficient decision algorithms for probabilistic simulations. Log. Methods Comput. Sci. 4(4:6) (2008)

    Google Scholar 

  88. Gallo, G., Grigoriadis, M.D., Tarjan, R.E.: A fast parametric maximum flow algorithm and applications. SIAM J. Comput. 18(1), 30–55 (1989)

    Article  MATH  MathSciNet  Google Scholar 

  89. Crafa, S., Ranzato, F.: Bisimulation and simulation algorithms on probabilistic transition systems by abstract interpretation. Form. Methods Syst. Des. 40(3), 356–376 (2012)

    Article  MATH  Google Scholar 

  90. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. Proceedings of the 4th ACM Symposium on Principles of Programming Languages, pp. 238–252. ACM (1977)

    Google Scholar 

  91. Panangaden, P.: Labelled Markov Processes. Imperial College Press, London (2009)

    Book  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Shanghai Jiao Tong University, Shanghai, China

    Yuxin Deng

Authors
  1. Yuxin Deng
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Yuxin Deng .

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Shanghai Jiao Tong University Press, Shanghai and Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Deng, Y. (2014). Probabilistic Bisimulation. In: Semantics of Probabilistic Processes. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-45198-4_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-45198-4_3

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-45197-7

  • Online ISBN: 978-3-662-45198-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation