Characterising Probabilistic Processes Logically

Abstract. 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.

• Type: Journal
• Year: 2010
• Where: CORR
• Authors: Yuxin Deng, Rob J. van Glabbeek
• Keywords: CORR 2010, Education, Probabilistic, Probabilistic Behaviour, Various Simulation-like Preorders