Sciweavers

FOSSACS
2007
Springer

Logical Characterizations of Bisimulations for Discrete Probabilistic Systems

14 years 5 months ago
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 ...
Augusto Parma, Roberto Segala
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where FOSSACS
Authors Augusto Parma, Roberto Segala
Comments (0)