On Inductive Characterization for Divergence-sensitive Probabilistic Branching Bisimilarity

Recently a divergence-sensitive branching bisimilarity has been proposed and studied for the randomized CCS model. In this paper, we give an equivalent inductive characterization for the bisimilarity, which is a probabilistic extension of the previous work on the non-probabilistic model. Based on the new characterization, a novel polynomial-time verification algorithm for the divergence-sensitive branching bisimilarity is proposed.