Weak Bisimulation is Sound and Complete for PCTL* Josee Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden
We investigate weak bisimulation of probabilistic systems in the
presence of nondeterminism, i.e. labelled concurrent Markov chains
(LCMC) with silent transitions. We build on the work of Philippou, Lee
and Sokolsky for finite state LCMCs. Their definition of weak
bisimulation destroys the additivity property of the probability
distributions, yielding instead capacities. The mathematics behind
capacities naturally captures the intuition that when we deal with
nondeterminism we must work with estimates on the possible
probabilities. Our analysis leads to three new developments:

concur02@fi.muni.cz 