Bisimulations Meet PCTL Equivalences for Probabilistic Automata

Probabilistic automata (PA) have beensuccessfully applied in the formal verification of concurrent andstochastic systems. Efficient model checking algorithms have beenstudied, where the most often used logics for expressing propertiesare based on PCTL and its extensionPCTL*. Variousbehavioral equivalences are proposed for PAs, asa powerful tool for abstraction and compositional minimization forPAs. Unfortunately, the behavioral equivalencesare well-known to be strictly stronger than the logical equivalences inducedby PCTL or PCTL*. This paper introduces novel notions of strongbisimulation relations, which characterizes PCTL and PCTL*exactly. We also extend weak bisimulations characterizingPCTL and PCTL* without next operator, respectively. Thus, ourpaper bridges the gap between logical and behavioral equivalences inthis setting.