Weak Bisimulation Metrics in Models with Nondeterminism and Continuous State Spaces

  • Ruggero Lanotte
  • Simone Tini
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11187)


Bisimulation metrics are used to estimate the behavioural distance between probabilistic systems. They have been defined in discrete and continuous state space models. However, the weak semantics approach, where non-observable actions are abstracted away, has been adopted only in the discrete case. We fill this gap and provide a weak bisimulation metric for models with continuous state spaces. A difficulty is to provide a notion of weak transition leaving from a continuous distribution over states. Our weak bisimulation metric allows for compositional reasoning. Systems at distance zero are equated by a notion of weak bisimulation. We apply our theory in a case study where continuous distributions derive by the evolution of the physical environment.


Weak bisimulation metric Nondeterminism Continuous state space 


  1. 1.
    Abate, A., Prandini, M., Lygeros, J., Sastry, S.: Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems. Automatica 44(11), 2724–2734 (2008). Scholar
  2. 2.
    Bravetti, M.: Specification and analysis of stochastic real-time systems. Ph.D. thesis, Università di Bologna (2002)Google Scholar
  3. 3.
    Bravetti, M., Gorrieri, R.: The theory of interactive generalized semi-Markov processes. Theor. Comput. Sci. 282(1), 5–32 (2002). Scholar
  4. 4.
    Bujorianu, M.L.: Extended stochastic hybrid systems and their reachability problem. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 234–249. Springer, Heidelberg (2004). Scholar
  5. 5.
    Bujorianu, M.L., Lygeros, J., Bujorianu, M.C.: Bisimulation for general stochastic hybrid systems. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 198–214. Springer, Heidelberg (2005). Scholar
  6. 6.
    Cattani, S., Segala, R., Kwiatkowska, M., Norman, G.: Stochastic transition systems for continuous state spaces and non-determinism. In: Sassone, V. (ed.) FoSSaCS 2005. LNCS, vol. 3441, pp. 125–139. Springer, Heidelberg (2005). Scholar
  7. 7.
    Chatzikokolakis, K., Gebler, D., Palamidessi, C., Xu, L.: Generalized bisimulation metrics. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 32–46. Springer, Heidelberg (2014). Scholar
  8. 8.
    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). Scholar
  9. 9.
    Deng, Y., Du, W.: The Kantorovich metric in computer science: a brief survey. Electron. Notes Theor. Comput. Sci. 253(3), 73–82 (2009). Scholar
  10. 10.
    Deng, Y., van Glabbeek, R.J., Hennessy, M., Morgan, C.: Characterising testing preorders for finite probabilistic processes. Log. Methods Comput. Sci. 4(4), Article no. 4 (2008).
  11. 11.
    Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. Theor. Comput. Sci. 318(3), 323–354 (2004). Scholar
  12. 12.
    Desharnais, J., Jagadeesan, R., Gupta, V., Panangaden, P.: The metric analogue of weak bisimulation for probabilistic processes. In: Proceedings of 17th Annual IEEE Symposium on Logic in Computer Science, LICS 2002, Copenhagen, July 2002, pp. 413–422. IEEE CS Press, Washington, DC (2002).
  13. 13.
    Du, W., Deng, Y., Gebler, D.: Behavioural pseudometrics for nondeterministic probabilistic systems. In: Fränzle, M., Kapur, D., Zhan, N. (eds.) SETTA 2016. LNCS, vol. 9984, pp. 67–84. Springer, Cham (2016). Scholar
  14. 14.
    Fränzle, M., Hahn, E.M., Hermanns, H., Wolovick, N., Zhang, L.: Measurability and safety verification for stochastic hybrid systems. In: Proceedings of 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, IL, April 2011, pp. 43–52. ACM Press, New York (2011).
  15. 15.
    Gebler, D., Larsen, K.G., Tini, S.: Compositional bisimulation metric reasoning with probabilistic process calculi. Log. Methods Comput. Sci. 12(4), Article no. 12 (2016).
  16. 16.
    Gebler, D., Tini, S.: SOS specifications for uniformly continuous operators. J. Comput. Syst. Sci. 92, 113–151 (2018). Scholar
  17. 17.
    Hahn, E.M., Hartmanns, A., Hermanns, H., Katoen, J.-P.: A compositional modelling and analysis framework for stochastic hybrid systems. Form. Methods Syst. Des. 43(2), 191–232 (2013). Scholar
  18. 18.
    Hennessy, M., Regan, T.: A process algebra for timed systems. Inf. Comput. 117(2), 221–23 (1995). Scholar
  19. 19.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)zbMATHGoogle Scholar
  20. 20.
    Hu, J., Lygeros, J., Sastry, S.: Towards a theory of stochastic hybrid systems. In: Lynch, N., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 160–173. Springer, Heidelberg (2000). Scholar
  21. 21.
    Lanotte, R., Merro, M.: A calculus of cyber-physical systems. In: Drewes, F., Martín-Vide, C., Truthe, B. (eds.) LATA 2017. LNCS, vol. 10168, pp. 115–127. Springer, Cham (2017). Scholar
  22. 22.
    Lanotte, R., Merro, M., Muradore, R., Viganò, L.: A formal approach to cyber-physical attacks. In: Proceedings of 30th IEEE Computer Security Foundations Symposium, CSF 2017, Santa Barbara, CA, August 2017, pp. 436–450. IEEE CS Press, Washington, DC (2017).
  23. 23.
    Lanotte, R., Merro, M., Tini, S.: Compositional weak metrics for group key update. In: Larsen, K.G., Bodlaender, H.L., Raskin, J.-F. (eds.) Proceedings of 42nd International Symposium on Mathematical Foundations of Computer Science, MFCS 2017. Leibniz International Proceedings in Informatics, Aalborg, August 2017, vol. 42, Article no. 72. Dagstuhl Publishing, Saarbrücken/Wadern (2017).
  24. 24.
    Lanotte, R., Merro, M., Tini, S.: Equational reasonings in wireless network gossip protocols. arXiv preprint 1707.03215 (2017).
  25. 25.
    Lanotte, R., Merro, M., Tini, S.: Weak simulation quasimetric in a gossip scenario. In: Bouajjani, A., Silva, A. (eds.) FORTE 2017. LNCS, vol. 10321, pp. 139–155. Springer, Cham (2017). Scholar
  26. 26.
    Lanotte, R., Merro, M., Tini, S.: Towards a formal notion of impact metric for cyber-physical attacks. In: Furia, C.A., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 296–315. Springer, Cham (2018). Scholar
  27. 27.
    Lanotte, R., Merro, M., Tini, S.: A probabilistic calculus of cyber-physical systems. Inf. Comput. (to appear)Google Scholar
  28. 28.
    Schiller, R.L.: Measures, Integrals and Martingales. Cambridge University Press, Cambridge (2005). Scholar
  29. 29.
    Segala, R.: Modeling and verification of randomized distributed real-time systems. Ph.D. thesis, MIT, Cambridge, MA (1995)Google Scholar
  30. 30.
    Sproston, J.: Decidable model checking of probabilistic hybrid automata. In: Joseph, M. (ed.) FTRTFT 2000. LNCS, vol. 1926, pp. 31–45. Springer, Heidelberg (2000). Scholar
  31. 31.
    van Breugel, F., Worrell, J.: A behavioural pseudometric for probabilistic transition systems. Theor. Comput. Sci. 331(1), 115–142 (2005). Scholar
  32. 32.
    Villani, C.: Optimal Transport, Old and New. Grundlehren der mathematischen Wissenschaften, vol. 338. Springer, Heidelberg (2008). Scholar
  33. 33.
    Wang, S., Zhan, N., Zhang, L.: A compositional modelling and verification framework for stochastic hybrid systems. Form. Aspects Comput. 29(4), 751–775 (2017). Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Dipartimento di Scienza e Alta TecnologiaUniversità degli Studi dell’InsubriaComoItaly

Personalised recommendations