A behavioural pseudometric for probabilistic transition systems
A behavioural pseudometric for probabilistic transition systems
复制标题
DOI：
10.1016/j.tcs.2004.09.035
复制
发表时间：
2005-02
期刊：
影响因子：
--
通讯作者：
F. Breugel;J. Worrell
中科院分区：
文献类型：
--
作者：
F. Breugel;J. Worrell
行为等价性的离散概念与以量化数据为特征的语义模型(如概率转换系统)格格不入。在这篇文章中，我们给出了一类概率转移系统上的伪距离，给出了行为等价的定量概念。基于度量空间上的Borel概率度量空间上的度量，通过函子的终端余代数定义伪度量。概率跃迁系统的态的距离为0当且仅当它们是概率双相似的。我们还用实值模态逻辑来刻画我们的距离函数。
Discrete notions of behavioural equivalence sit uneasily with semantic models featuring quantitative data, like probabilistic transition systems. In this paper, we present a pseudometric on a class of probabilistic transition systems yielding a quantitative notion of behavioural equivalence. The pseudometric is defined via the terminal coalgebra of a functor based on a metric on the space of Borel probability measures on a metric space. States of a probabilistic transition system have distance 0 if and only if they are probabilistic bisimilar. We also characterize our distance function in terms of a real-valued modal logic.