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.
翻译:双模拟是捕获各类转移系统中状态行为等价性的一种概念。该概念在强调步骤基本性的离散时间框架下已得到广泛研究。在我们的设定中,我们考虑的是强调连续时间演化的"流"过程。在此类连续时间设定下,相关概念并非离散时间情形的简单推广,因此我们将研究范围限定于随时间无质量损耗且满足额外正则性条件的扩散过程。此前工作中,我们针对演化呈现时间流特征的连续时间随机过程提出了不同定义的行为等价性概念,但该工作仅涉及等价关系。本研究旨在量化不同过程的行为差异程度,为此我们提出了两种适用于类扩散过程的伪度量。这些伪度量是状态空间上有界为1的伪度量空间中两个不同泛函的不动点。我们还通过实值模态逻辑对这些伪度量进行刻画——这对应了双模拟逻辑刻画概念的定量类比。这些实值模态逻辑表明两种伪度量存在差异,因而衍生出不同的行为等价性概念。