|
Logic & Semantics |
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.)