A behavioural pseudometric for continuous-time Markov processes

TL;DR

This paper introduces a new behavioral pseudometric for continuous-time Markov processes, extending bisimulation metrics from discrete to continuous time, using fixpoint and logical approaches.

Contribution

It generalizes bisimulation metrics to continuous-time processes, unifying fixpoint and logical characterizations for such systems.

Findings

Defined a behavioral pseudometric for continuous-time processes

Proved the equivalence of fixpoint and logical approaches

Applicable to processes like Brownian motion and jump processes

Abstract

In this work, we generalize the concept of bisimulation metric in order to metrize the behaviour of continuous-time processes. Similarly to what is done for discrete-time systems, we follow two approaches and show that they coincide: as a fixpoint of a functional and through a real-valued logic. The whole discrete-time approach relies entirely on the step-based dynamics: the process jumps from state to state. We define a behavioural pseudometric for processes that evolve continuously through time, such as Brownian motion or involve jumps or both.