Behavioural Equivalences for Probabilistic Systems

In recent years the need for reasoning about probabilistic behaviour, as exhibited for instance in randomized, distributed and fault-tolerant systems, has triggered much interest in the area of formal methods for the specification and analysis of probabilistic systems. As a result various formal models have been proposed and studied and verification techniques for them have been developed.

In this talk I will consider behavioural equivalences in the framework of Labelled Concurrent Markov Chains, LCMC's, that is, transition systems which exhibit both probabilistic and nondeterministic behavior. In particular, I will introduce the notion of weak bisimulation, an equivalence relation which abstracts from internal computation of systems, for the model. The definition employs the notion of a 'scheduler', an entity that resolves the nondeterminism present in an LCMC, thus decomposing it into a possibly infinite number of computation trees. I will show that in order to compute weak bisimulation it is sufficient to restrict attention to only a finite number of these computations. Finally, I will present an algorithm for deciding weak bisimulation which works in polynomial time in the number of states of the transition system.
(This is joint work with Oleg Sokolsky, University of Pennsylvania.)

LS Home page or Talks in 1998/99