Behavioural Pseudometrics for Nondeterministic Probabilistic Systems

  • Wenjie Du
  • Yuxin DengEmail author
  • Daniel Gebler
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9984)


For the model of probabilistic labelled transition systems that allow for the co-existence of nondeterminism and probabilities, we present two notions of bisimulation metrics: one is state-based and the other is distribution-based. We provide a sound and complete modal characterisation for each of them, using real-valued modal logics based on Hennessy-Milner logic. The logic for characterising the state-based metric is much simpler than an earlier logic by Desharnais et al. as it uses only two non-expansive operators rather than the general class of non-expansive operators. For the kernels of the two metrics, which correspond to two notions of bisimilarity, we give a comprehensive comparison with some typical distribution-based bisimilarities in the literature.



We thank the anonymous referees for their helpful comments.


  1. 1.
    Castiglioni, V., Gebler, D., Tini, S.: Logical characterization of bisimulation metrics. In: Proceedings of QAPL 2016. EPTCS (2016)Google Scholar
  2. 2.
    Chatterjee, K., De Alfaro, L., Majumdar, R., Raman, V.: Algorithms for game metrics. Log. Methods Comput. Sci. 6(3:13), 1–27 (2010)MathSciNetzbMATHGoogle Scholar
  3. 3.
    Cleaveland, R., Iyer, S.P., Narasimha, M.: Probabilistic temporal logics via the modal mu-calculus. Theor. Comput. Sci. 342(2–3), 316–350 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    D’Argenio, P.R., Sánchez Terraf, P., Wolovick, N.: Bisimulations for non-deterministic labelled Markov processes. Math. Struct. Comput. Sci. 22(1), 43–68 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    De Alfaro, L., Faella, M., Stoelinga, M.: Linear and branching system metrics. IEEE Trans. Softw. Eng. 35(2), 258–273 (2009)CrossRefzbMATHGoogle Scholar
  6. 6.
    De Alfaro, L., Majumdar, R., Raman, V., Stoelinga, M.: Game relations and metrics. In: Proceedings of LICS 2007, pp. 99–108. IEEE (2007)Google Scholar
  7. 7.
    De Alfaro, L., Majumdar, R., Raman, V., Stoelinga, M.: Game refinement relations and metrics. Log. Methods Comput. Sci. 4(3:7), 1–28 (2008)MathSciNetzbMATHGoogle Scholar
  8. 8.
    de Vink, E.P., Rutten, J.J.M.M.: Bisimulation for probabilistic transition systems: a coalgebraic approach. Theor. Comput. Sci. 221(1/2), 271–293 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  9. 9.
    den Hartog, J.I.: Probabilistic Extensions of Semantical Models. Ph.D. thesis, Free University Amsterdam (2002)Google Scholar
  10. 10.
    Deng, Y.: Semantics of Probabilistic Processes: An Operational Approach. Springer, Heidelberg (2015)Google Scholar
  11. 11.
    Deng, Y., Chothia, T., Palamidessi, C., Pang, J.: Metrics for action-labelled quantitative transition systems. ENTCS 153(2), 79–96 (2006)Google Scholar
  12. 12.
    Deng, Y., Du, W.: Logical, metric, and algorithmic characterisations of probabilistic bisimulation. Technical report CMU-CS-11-110, Carnegie Mellon University, March 2011Google Scholar
  13. 13.
    Deng, Y., Feng, Y., Dal Lago, U.: On coinduction and quantum lambda calculi. In: Proceedings of CONCUR 2015, pp. 427–440. LIPIcs (2015)Google Scholar
  14. 14.
    Deng, Y., Hennessy, M.: On the semantics of Markov automata. Inf. Comput. 222, 139–168 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Deng, Y., Glabbeek, R., Hennessy, M., Morgan, C.: Testing finitary probabilistic processes. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 274–288. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-04081-8_19 CrossRefGoogle Scholar
  16. 16.
    Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. Theor. Comput. Sci. 318(3), 323–354 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Desharnais, J., Jagadeesan, R., Gupta, V., Panangaden, P.: The metric analogue of weak bisimulation for probabilistic processes. In: Proceedings of LICS 2002, pp. 413–422. IEEE (2002)Google Scholar
  18. 18.
    Eisentraut, C., Godskesen, J.C., Hermanns, H., Song, L., Zhang, L.: Probabilistic bisimulation for realistic schedulers. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 248–264. Springer, Heidelberg (2015). doi: 10.1007/978-3-319-19249-9_16 CrossRefGoogle Scholar
  19. 19.
    Fahrenberg, U., Legay, A.: The quantitative linear-time branching-time spectrum. Theor. Comput. Sci. 538, 54–69 (2014)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Feng, Y., Ying, M.: Toward automatic verification of quantum cryptographic protocols. In: Proceedings of CONCUR 2015. LIPIcs, vol. 42, pp. 441–455 (2015)Google Scholar
  21. 21.
    Feng, Y., Zhang, L.: When equivalence and bisimulation join forces in probabilistic automata. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 247–262. Springer, Heidelberg (2014). doi: 10.1007/978-3-319-06410-9_18 CrossRefGoogle Scholar
  22. 22.
    Ferns, N., Panangaden, P., Precup, D.: Bisimulation metrics for continuous Markov decision processes. SIAM J. Comput. 40(6), 1662–1714 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  23. 23.
    Ferns, N., Precup, D., Knight, S.: Bisimulation for Markov decision processes through families of functional expressions. In: Breugel, F., Kashefi, E., Palamidessi, C., Rutten, J. (eds.) Horizons of the Mind. A Tribute to Prakash Panangaden: Essays Dedicated to Prakash Panangaden on the Occasion of His 60th Birthday. LNCS, vol. 8464, pp. 319–342. Springer, Heidelberg (2014). doi: 10.1007/978-3-319-06880-0_17 CrossRefGoogle Scholar
  24. 24.
    Gebler, D., Larsen, K.G., Tini, S.: Compositional metric reasoning with probabilistic process calculi. In: Pitts, A. (ed.) FoSSaCS 2015. LNCS, vol. 9034, pp. 230–245. Springer, Heidelberg (2015). doi: 10.1007/978-3-662-46678-0_15 CrossRefGoogle Scholar
  25. 25.
    Giacalone, A., Jou, C., Smolka, S.: Algebraic reasoning for probabilistic concurrent systems. In: Proceedings of IFIP TC2 Working Conference on Programming Concepts and Methods, pp. 443–458 (1990)Google Scholar
  26. 26.
    Hennessy, M.: Exploring probabilistic bisimulations, part I. Formal Aspects Comput. 24(4–6), 749–768 (2012)MathSciNetCrossRefzbMATHGoogle Scholar
  27. 27.
    Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32, 137–161 (1985)MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Hermanns, H., Krčál, J., Křetínský, J.: Probabilistic bisimulation: naturally on distributions. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 249–265. Springer, Heidelberg (2014). doi: 10.1007/978-3-662-44584-6_18 Google Scholar
  29. 29.
    Huth, M., Kwiatkowska, M.Z.: Quantitative analysis and model checking. In: Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, pp. 111–122. IEEE Computer Society (1997)Google Scholar
  30. 30.
    Jonsson, B., Larsen, K.G., Yi, W.: Probabilistic extensions of process algebras. In: Handbook of Process Algebra, pp. 685–710. Elsevier, Amsterdam (2001)Google Scholar
  31. 31.
    Kantorovich, L., Rubinshtein, G.: On a space of totally additive functions. Vestn Len. Univ. 13(7), 52–59 (1958)zbMATHGoogle Scholar
  32. 32.
    Kozen, D.: Results on the propositional mu-calculus. Theor. Comput. Sci. 27, 333–354 (1983)MathSciNetCrossRefzbMATHGoogle Scholar
  33. 33.
    Kwiatkowska, M., Norman, G.: Probabilistic metric semantics for a simple language with recursion. In: Penczek, W., Szałas, A. (eds.) MFCS 1996. LNCS, vol. 1113, pp. 419–430. Springer, Heidelberg (1996). doi: 10.1007/3-540-61550-4_167 CrossRefGoogle Scholar
  34. 34.
    Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94, 1–28 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  35. 35.
    Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1991)zbMATHGoogle Scholar
  36. 36.
    Norman, G.J.: Metric Semantics for Reactive Probabilistic Systems. Ph.D. thesis, University of Birmingham (1997)Google Scholar
  37. 37.
    Philippou, A., Lee, I., Sokolsky, O.: Weak bisimulation for probabilistic systems. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 334–349. Springer, Heidelberg (2000). doi: 10.1007/3-540-44618-4_25 Google Scholar
  38. 38.
    Raman, V.: Game Relations, Metrics and Refinements. Ph.D. thesis, University of California (2010)Google Scholar
  39. 39.
    Segala, R.: Modeling and Verification of Randomized Distributed Real-Time Systems. Ph.D. thesis, MIT (1995)Google Scholar
  40. 40.
    Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 481–496. Springer, Heidelberg (1994). doi: 10.1007/978-3-540-48654-1_35 Google Scholar
  41. 41.
    Song, L., Deng, Y., Cai, X.: Towards automatic measurement of probabilistic processes. In: Proceedings of QSIC 2007, pp. 50–59. IEEE (2007)Google Scholar
  42. 42.
    van Breugel, F., Sharma, B., Worrell, J.: Approximating a behavioural pseudometric without discount for probabilistic systems. Log. Methods Comput. Sci. 4(2:2), 1–23 (2008)MathSciNetzbMATHGoogle Scholar
  43. 43.
    Breugel, F., Worrell, J.: An algorithm for quantitative verification of probabilistic transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 336–350. Springer, Heidelberg (2001). doi: 10.1007/3-540-44685-0_23 Google Scholar
  44. 44.
    Breugel, F., Worrell, J.: Towards quantitative verification of probabilistic transition systems. In: Orejas, F., Spirakis, P.G., Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 421–432. Springer, Heidelberg (2001). doi: 10.1007/3-540-48224-5_35 CrossRefGoogle Scholar
  45. 45.
    van Breugel, F., Worrell, J.: A behavioural pseudometric for probabilistic transition systems. Theor. Comput. Sci. 331(1), 115–142 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  46. 46.
    Ying, M.: Bisimulation indexes and their applications. Theor. Comput. Sci. 275(1/2), 1–68 (2002)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG 2016

Authors and Affiliations

  1. 1.Shanghai Normal UniversityShanghaiChina
  2. 2.Shanghai Key Laboratory of Trustworthy ComputingEast China Normal UniversityShanghaiChina
  3. 3.VU University AmsterdamAmsterdamNetherlands

Personalised recommendations