A weak semantic approach to bisimulation metrics in models with nondeterminism and continuous state spaces

Bisimulation metrics are a successful instrument used to estimate the behavioural distance between probabilistic concurrent systems. They have been defined in both 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. In this paper we fill this gap and provide a weak bisimulation metric for models with continuous state spaces. A technical difficulty is to provide a suitable notion of weak transition, which requires to lift transitions leaving from states to transitions leaving from a continuous distribution over states. We prove that our weak bisimulation metric is non-expansive, thus allowing for compositional reasoning. We prove that systems at distance zero are equated by a suitable notion of probabilistic weak bisimulation. We apply our theory in a case study where continuous distributions derive from the evolution of the physical environment