Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Behavioural pseudometrics for continuous-time diffusions

Linan Chen, Florence Clerc, Prakash Panangaden

TL;DR

This work develops two quantitative behavioural metrics for continuous-time diffusions, distinguishing true flow dynamics from step-based notions. One metric is fixpoint-based and kernel-driven, the other hinges on trajectory transport, with each having a corresponding real-valued logic that characterizes the distance. The authors prove that each metric equals its logic-derived counterpart, establishing a precise logical semantics for continuous-time behavioural distance. The framework relies on lower semi-continuity, couplings, and Kantorovich duality to craft Wasserstein-type distances over kernels and trajectory measures, and it uses a discount parameter to ensure continuity of iterates. The results provide a rigorous foundation for measuring how differently diffusion processes behave and open avenues for relaxing assumptions and extending to broader classes of stochastic flows.

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 a discrete-time setting where the notion of a step is fundamental. In our setting we are considering "flow"-processes emphasizing that they evolve in continuous time. In such continuous-time settings, the concepts are not straightforward adaptations of their discrete-time analogues and we restrict our study to diffusions that do not lose mass over time and with additional regularity constraints. In previous work we proposed different definitions of behavioural equivalences for continuous-time stochastic processes where the evolution is a flow through time. That work only addressed equivalences. In this work, we aim at quantifying how differently processes behave. We present two pseudometrics for diffusion-like processes. These pseudometrics are fixpoints of two different functionals on the space of 1-bounded pseudometrics on the state space. We also characterize these pseudometrics in terms of real-valued modal logics; this is a quantitative analogue of the notion of logical characterization of bisimulation. These real-valued modal logics indicate that the two pseudometrics are different and thus yield different notions of behavioural equivalence.

Behavioural pseudometrics for continuous-time diffusions

TL;DR

This work develops two quantitative behavioural metrics for continuous-time diffusions, distinguishing true flow dynamics from step-based notions. One metric is fixpoint-based and kernel-driven, the other hinges on trajectory transport, with each having a corresponding real-valued logic that characterizes the distance. The authors prove that each metric equals its logic-derived counterpart, establishing a precise logical semantics for continuous-time behavioural distance. The framework relies on lower semi-continuity, couplings, and Kantorovich duality to craft Wasserstein-type distances over kernels and trajectory measures, and it uses a discount parameter to ensure continuity of iterates. The results provide a rigorous foundation for measuring how differently diffusion processes behave and open avenues for relaxing assumptions and extending to broader classes of stochastic flows.

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 a discrete-time setting where the notion of a step is fundamental. In our setting we are considering "flow"-processes emphasizing that they evolve in continuous time. In such continuous-time settings, the concepts are not straightforward adaptations of their discrete-time analogues and we restrict our study to diffusions that do not lose mass over time and with additional regularity constraints. In previous work we proposed different definitions of behavioural equivalences for continuous-time stochastic processes where the evolution is a flow through time. That work only addressed equivalences. In this work, we aim at quantifying how differently processes behave. We present two pseudometrics for diffusion-like processes. These pseudometrics are fixpoints of two different functionals on the space of 1-bounded pseudometrics on the state space. We also characterize these pseudometrics in terms of real-valued modal logics; this is a quantitative analogue of the notion of logical characterization of bisimulation. These real-valued modal logics indicate that the two pseudometrics are different and thus yield different notions of behavioural equivalence.
Paper Structure (43 sections, 57 theorems, 43 equations)

This paper contains 43 sections, 57 theorems, 43 equations.

Table of Contents

  1. Introduction
  2. Mathematical background
  3. Lower semi-continuity
  4. Couplings
  5. Optimal transport theory
  6. The processes we consider: diffusions
  7. Definition of Feller-Dynkin Process
  8. Trajectories
  9. Diffusions
  10. Observables
  11. Defining a pseudometric through functionals
  12. On the set of pseudometrics
  13. Defining our functional
  14. When restricted to continuous pseudometrics
  15. Defining our family of pseudometrics
  16. ...and 28 more sections

Key Result

Lemma 2.1

Assume there is an arbitrary family of continuous functions $f_i : X \mathrel { \mathop{\hbox{\rightarrowfill}}\limits }\mathbb{R}$ ($i \in \mathcal{I}$) and define $f(x) = \sup_{i \in \mathcal{I}} f_i(x)$ for every $x \in X$. Then $f$ is lower semi-continuous.

Theorems & Definitions (73)

  • Definition 2.1
  • Lemma 2.1
  • Theorem 2.2
  • Definition 2.3
  • Lemma 2.3
  • Remark 2.4
  • Lemma 2.4
  • Lemma 2.4
  • Definition 3.1
  • Definition 3.2
  • ...and 63 more