  Probabilistic automata (PAs) have been successfully applied in 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 probabilistic computation tree logic (PCTL) and its
extension PCTL^*. Various behavioral equivalences are proposed, as a powerful
tool for abstraction and compositional minimization for PAs. Unfortunately, the
equivalences are well-known to be sound, but not complete with respect to the
logical equivalences induced by PCTL or PCTL*. The desire of a both sound and
complete behavioral equivalence has been pointed out by Segala in 1995, but
remains open throughout the years. In this paper we introduce novel notions of
strong bisimulation relations, which characterize PCTL and PCTL* exactly. We
extend weak bisimulations that characterize PCTL and PCTL* without next
operator, respectively. Further, we also extend the framework to simulation
preorders. Thus, our paper bridges the gap between logical and behavioral
equivalences and preorders in this setting.
