期刊
FORMAL ASPECTS OF COMPUTING
卷 24, 期 4-6, 页码 749-768出版社
SPRINGER
DOI: 10.1007/s00165-012-0242-7
关键词
Probabilistic processes; Contextual equivalence; Bisimulation equivalence; Logical characterisation; Equational theory
资金
- SFI [SFI 06 IN.1 1898]
We take a fresh look at strong probabilistic bisimulations for processes which exhibit both non-deterministic and probabilistic behaviour. We suggest that it is natural to interpret such processes as distributions over states in a probabilistic labelled transition system, a pLTS; this enables us to adapt the standard notion of contextual equivalence to this setting. We then prove that a novel form of bisimulation equivalence between distributions are both sound and complete with respect to this contextual equivalence. We also show that a very simple extension to HML, Hennessy-Milner Logic, provides finite explanations for inequivalences between distributions. Finally we show that our bisimulations between distributions in a pLTS are simply an alternative characterisation of a standard notion of probabilistic bisimulation equivalence, defined between states in a pLTS.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据