Probabilistic Extensions of Process Algebras

In this chapter, we adopt Probabilistic Transition Systems as a basic model for probabilistic processes, in which probabilistic and nondeterministic choices are independent concepts. The model is essentially a nondeterministic version of Markov decision processes or probabilistic automata of Rabin. We develop a general framework to define probabilistic process languages to describe probabilistic transition systems. In particular, we show how operators for nonprobabilistic process algebras can be lifted to probabilistic process algebras in a uniform way similar to de Simone format. To establish a notion of refinement, we present a family of preorders including probabilistic bisimulation and simulation, and probabilistic testing pre-orders as well as their logical or denotational characterization. These preorders are shown to be precongruences with respect to the algebraic operators that can be defined in our general framework. Finally, we give a short account of the important work on extending the successful field of model checking to probabilistic settings and a brief discussion on current research in the area.