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: