Probabilistic automata (PA) have been successfully applied in the formal
verification of concurrent and stochastic systems. Efficient model checking
algorithms have been studied, where the most often used logics for expressing
properties are based on PCTL and its extension PCTL*. Various behavioral
equivalences are proposed for PAs, as a powerful tool for abstraction and
compositional minimization for PAs. Unfortunately, the behavioral equivalences
are well-known to be strictly stronger than the logical equivalences induced by
PCTL or PCTL*.