Bisimulation for Feller-Dynkin Processes
Linan Chen, Florence Clerc, Prakash Panangaden
TL;DR
This work develops a rigorous theory of bisimulation for continuous-time stochastic processes, focusing on Feller-Dynkin processes to capture true time-flow evolution. It introduces two definitions of bisimulation that are shown to be equivalent and demonstrates how they specialize to the standard discrete-time notion, while not being a naive extension. The trajectory-based bisimulation is complemented by a FD-homomorphism and pushout (cospan) framework, establishing a robust, compositional view of behavioural equivalence across possibly different state spaces. Through extensive Brownian-motion-based examples, the authors illustrate the discriminative power and structural properties of the proposed notions and lay groundwork for quantitative metrics and logical characterizations of continuous-time bisimulation with practical verification implications.
Abstract
Bisimulation is a concept that captures behavioural equivalence. It has been studied extensively on nonprobabilistic systems and on discrete-time Markov processes and on so-called continuous-time Markov chains. In the latter time is continuous but the evolution still proceeds in jumps. We propose two definitions of bisimulation on continuous-time stochastic processes where the evolution is a \emph{flow} through time. We show that they are equivalent and we show that when restricted to discrete-time, our concept of bisimulation encompasses the standard discrete-time concept. The concept we introduce is not a straightforward generalization of discrete-time concepts.