Logical Characterizations of Bisimulations for Discrete Probabilistic Systems

Appears:Proceedings of the 10th International Conference on Foundations of Software Science and Computational Structures (FOSSACS), Braga, Portugal, LNCS 4423, pages 287-301, April 2007.

Abstract: 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 in 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 single probabilistic transition.

Download:
Download the paper from the publisher.

Download an author-created copy of the paper (© Springer-Verlag).