Characterising Probabilistic Processes Logically. Available at http://arxiv.org/abs/1007.5188. Full version of this paper

Abstract. In this paper we work on (bi)simulation semantics of pro-cesses 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.