Weak Bisimulation for Fully Probabilistic Processes

Christel BaierChristel Baier, Holger HermannsHolger Hermanns

Christel Baier, Holger Hermanns
Weak Bisimulation for Fully Probabilistic Processes
Formale Beschreibungstechniken für verteilte Systeme, GI/ITG-Fachgespräch, Berlin, 19.-20. Juni 1997, volume 315 of GMD-Studien, 59--68, 1997. GMD-Forschungszentrum Informationstechnik GmbH

Details
Bibtex

KurzfassungAbstract
Bisimulations that abstract from internal computation have proven to be useful for verification of compositionally defined transition system. In the literature of probabilistic extensions of such transition systems, similar bisimulations are rare. In this paper, we introduce weak bisimulation and branching bisimulation for transition systems where nondeterministic branching is replaced by probabilistic branching. In contrast to the nondeterministic case, both relations coincide. We give an algorithm to decide weak bisimulation with a time complexity cubic in the number of states of the transition system. This meets the worst case complexity for deciding branching bisimulation in the nondeterministic case.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

@inproceedings{BH1997,
  author    = {Christel Baier and Holger Hermanns},
  title     = {Weak Bisimulation for Fully Probabilistic Processes},
  booktitle = {Formale Beschreibungstechniken f{\"{u}}r verteilte Systeme,
               {GI/ITG-Fachgespr{\"{a}}ch,} Berlin, 19.-20. Juni 1997},
  series    = {GMD-Studien},
  volume    = {315},
  publisher = {GMD-Forschungszentrum Informationstechnik {GmbH}},
  year      = {1997},
  pages     = {59--68}
}