Advertisement

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)

Abstract

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.

Notes

Acknowledgement

We thank the anonymous referees for their helpful comments.

References

  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