Two behavioural pseudometrics for continuous-time Markov processes
Linan Chen, Florence Clerc, Prakash Panangaden
TL;DR
The paper extends behavioural quantification to continuous-time Markov processes by introducing two complementary pseudometrics: a kernel-based distance δ̄^c and a trajectory-based distance overline{d}^c. Each distance is constructed in two ways: via a functional (F_c for kernels and G_c for trajectories) and via a real-valued logic (Λ and ell^c), with rigorous fixpoint results equating the two perspectives in each framework. It further clarifies the relationship between the kernel- and trajectory-based metrics, proving δ̄^c ≤ overline{d}^c in general and showing both can be strictly different, depending on process dynamics. The work also develops a two-part real-valued logic to handle state-and-trajectory tests, provides approximation techniques, and illustrates the theory with Brownian-motion-inspired examples, highlighting the richer discriminative power of trajectory-based approaches in continuous time.
Abstract
Bisimulation is a concept that captures behavioural equivalence of states in a variety of types of transition systems. It has been widely studied in discrete-time settings where a key notion is the bisimulation metric which quantifies "how similar two states are". In [ 11], we generalized the concept of bisimulation metric in order to metrize the behaviour of continuous-time Markov processes. Similarly to the discrete-time case, we constructed a pseudometric following two iterative approaches - through a functional and through a real-valued logic, and showed that the outcomes coincide: the pseudometric obtained from the logic is a specific fixpoint of the functional which yields our first pseudometric. However, different from the discrete-time setting, in which the process has a step-by-step dynamics, the behavioural pseudometric we constructed applies to Markov processes that evolve continuously through time, such as diffusions and jump diffusions. While our treatment of the pseudometric in [11] relied on the time-indexed Markov kernels, in [ 8 , 9, 10 ], we showed the importance of trajectories in the consideration of behavioural equivalences for true continuous-time Markov processes. In this paper, we take the work from [11 ] further and propose a second behavioural pseudometric for diffusions based on trajectories. We conduct a similar study of this pseudometric from both the perspective of a functional and the viewpoint of a real-valued logic. We also compare this pseudometric with the first pseudometric obtained in [11].