Logical Characterizations of Bisimulations for Discrete Probabilistic Systems

We give logical characterizations of bisimulation relations for the probabilistic automata of Segala in terms of three Hennessy-Milner style logics. The three logics characterize strong, strong probabilistic and weak probabilistic bisimulation, and differ only for the kind of diamond operator used. Compared to the Larsen and Skou logic for reactive systems, these logics introduce a new operator that measures the probability of the set of states that satisfy a formula. Moreover, the satisfaction relation is defined on measures rather than single states. We rederive previous results of Desharnais et. al. by defining sublogics for Reactive and Alternating Models viewed as restrictions of probabilistic automata. Finally, we identify restrictions on probabilistic automata, weaker than those imposed by the Alternating Models, that preserve the logical characterization of Desharnais et. al. These restrictions require that each state either enables several ordinary transitions or enables a ...

• Type: Conference
• Year: 2007
• Where: FOSSACS
• Authors: Augusto Parma, Roberto Segala
• Keywords: Applied Computing, FOSSACS 2007, Probabilistic, Probabilistic Automata, Weak Probabilistic Bisimulation