Characterising Probabilistic Processes Logically
                      (Extended Abstract)

              Yuxin Deng and Rob van Glabbeek

In this paper we work on (bi)simulation semantics of processes that
exhibit both nondeterministic and probabilistic behaviour.
We propose a probabilistic extension of the modal mu-calculus and show
how to derive characteristic formulae for various simulation-like
preorders over finite-state processes without divergence.
In addition, we show that even without the fixpoint operators
this probabilistic mu-calculus can be used to characterise these
behavioural relations in the sense that two states are equivalent
if and only if they satisfy the same set of formulae.