Branching and weak probabilistic bisimilarities are two well-known notions capturing behavioral equivalence between nondeterministic probabilistic systems. For probabilistic systems, divergence is of major concern. Recently several divergence-sensitive refinements of branching and weak probabilistic bisimilarities have been proposed in the literature. Both the definitions of these equivalences and the techniques to investigate them differ significantly. This paper presents a comprehensive comparative study on divergence-sensitive behavioral equivalence relations that refine the branching and weak probabilistic bisimilarities. Additionally, these equivalence relations are shown to have efficient checking algorithms. The techniques of this paper might be of independent interest in a more general setting.

翻译：摘要：分支概率互模拟与弱概率互模拟是刻画非确定性概率系统行为等价性的两种经典概念。在概率系统中，发散性是一个关键问题。近年来，文献中提出了多种针对发散性敏感的分支概率互模拟与弱概率互模拟的改进形式，这些等价关系的定义及其研究方法存在显著差异。本文对基于分支概率互模拟与弱概率互模拟的发散性敏感行为等价关系进行了系统比较研究。此外，本文证明了这些等价关系存在高效验证算法。本文所提出的技术方法在更广泛的场景中可能具有独立的研究价值。