Analyzing Divergence for Nondeterministic Probabilistic Models
Hao Wu, Yuxi Fu, Huan Long, Xian Xu, Wenbo Zhang
TL;DR
This paper addresses divergence sensitivity in probabilistic nondeterministic models by comparing branching and weak bisimulation refinements that account for divergence. It introduces two divergence-sensitive notions for RCCS_fs: branching bisimulation with explicit divergence ($\simeq^{\Delta}$) and exhaustive branching bisimulation ($\simeq_{e}$), each capturing different divergence aspects via divergent $\epsilon$-trees and maximal $\tau$-ECs, respectively. The authors establish a lattice of relations among these variants, showing, for example, that $\simeq^{\Delta} \subsetneq \simeq_{e} \subsetneq \simeq \subsetneq \approx$ and that $\simeq_{e} \subseteq \approx_{e}$, with strict separations demonstrated by concrete examples. They provide polynomial-time algorithms for all divergence-sensitive notions, including DetDivTree, DivBranBisim, ExhBranBisim, and ExhWeakBisim, and demonstrate how distribution-based and $\epsilon$-tree based semantics can be related algorithmically. The work advances practical verification of divergence-sensitive probabilistic processes and suggests broad applicability to other probabilistic models and future axiomatizations.
Abstract
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.